{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:34:13Z","timestamp":1694622853928},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2004,4,1]],"date-time":"2004-04-01T00:00:00Z","timestamp":1080777600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2004,4]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>The bulk synchronous parallel (BSP) model is underpinned by a global synchronisation operation. This operation both synchronises processes and updates local stores using asynchronous communications. In this paper a generalised, nondeterministic, substitution axiom (over functions) is identified with BSP barrier synchronisation. Correctness proofs of BSP programs based on the axiom are structurally similar to proofs of correctness of sequential programs. Global synchronisation is often considered to be relatively expensive to implement on distributed architectures for applications having low levels of communications. In an extreme situation a process having no external interactions may have to wait unnecessarily at a barrier. In this paper a form of barrier operation is introduced which is straightforward to reason about and, with a view to increasing the potential for efficient implementation, permits barrier operations to be relaxed through partial uncoupling thereby allowing processes which do not need to synchronise to proceed.<\/jats:p>","DOI":"10.1007\/s00165-004-0028-7","type":"journal-article","created":{"date-parts":[[2004,3,29]],"date-time":"2004-03-29T12:36:13Z","timestamp":1080563773000},"page":"36-50","source":"Crossref","is-referenced-by-count":6,"title":["Barrier synchronisation: Axiomatisation and relaxation"],"prefix":"10.1145","volume":"16","author":[{"given":"A.","family":"Stewart","sequence":"first","affiliation":[{"name":"School of Computer Science, The Queen\u2019s University of Belfast, Northern Ireland, Belfast"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Clint","sequence":"additional","affiliation":[{"name":"School of Computer Science, The Queen\u2019s University of Belfast, Northern Ireland, Belfast"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Gabarr\u00f3","sequence":"additional","affiliation":[{"name":"Department of LSI, Universitat Polit\u00e8cnica de Catalunya, Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","doi-asserted-by":"crossref","first-page":"804","DOI":"10.1145\/4221.4227","article-title":"Complexity of network synchronization","volume":"32","author":"Awe B","year":"1985","journal-title":"JACM"},{"key":"p_2","volume-title":"Lecture notes in computer science, vol 1196"},{"key":"p_3","first-page":"46","volume-title":"In: Design, implementation","author":"New York","year":"1999"},{"key":"p_4","volume-title":"Formal validation of data-parallel programs: a two-component","author":"Bou L","year":"1997"},{"key":"p_5","unstructured":"assertional proof system for a simple language.\n  Theor Comput Sci 189:71-107 [ChS01] Chen Y Sanders JW (2001) Logic of global synchrony. CONCUR\n  2001\n  :\n  487\n  -\n  501\n   [dlT96] de la Torre P Kruskal CP\n   (\n  1996\n  ) Submachine locality in the bulk synchronous setting. \n  In\n  : Euro-Par'96. \n  Lecture\n   notes in"},{"key":"p_6","first-page":"352","volume-title":"vol 1124","year":"2001"},{"key":"p_7","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1145\/69610.357988","article-title":"Predicative programming, part 1","volume":"27","author":"Euro-Par'","year":"1984","journal-title":"Commun ACM"},{"key":"p_8","first-page":"576","article-title":"-1980 [Hoa69] Hoare CAR (1969) An axiomatic basis for computer programming","volume":"12","author":"Parallel Comput","year":"1947","journal-title":"Commun ACM"},{"issue":"1","key":"p_9","first-page":"253","article-title":"A calculus of BSP programs","volume":"37","author":"Inf Process Lett F","year":"2000","journal-title":"Sci Comput Program"},{"key":"p_10","first-page":"46","volume-title":"vol 1000","author":"Lecture","year":"2001"},{"key":"p_11","doi-asserted-by":"crossref","unstructured":"43:77-89 [MPI95] MPI\n  : \n  a message-passing interface standard University of Tennessee (1995) [Ski97] Skillicorn DB Hill JMD McColl WF (1997) Questions and answers about BSP. Sci Program\n  6\n  :\n  249\n  -\n  274\n   [StC97] Stewart A Clint\n   M (\n  1997\n  ) Synchronising asynchronous communications. \n  In\n  : Lengauer C Griebl M Gorlatch S (eds) \n  Euro","DOI":"10.1155\/1997\/532130"},{"key":"p_12","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1093\/comjnl\/44.3.174","article-title":"BSP-style computation: a semantic investigation","volume":"44","author":"Par'","year":"2001","journal-title":"Comput J"},{"key":"p_13","volume-title":"Gorlatch S, Lengauer C (eds)","author":"Stewart A","year":"2002"},{"key":"p_14","first-page":"41","volume-title":"Nova Science","author":"Constructive","year":"2001"},{"key":"p_15","volume-title":"Sakellariou R, Keane J, Gurd J","year":"2001"},{"issue":"8","key":"p_16","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1145\/79173.79181","article-title":"A bridging model for parallel computation","volume":"33","author":"Springer","year":"1990","journal-title":"Commun ACM"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-004-0028-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-004-0028-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-004-0028-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:36:01Z","timestamp":1641483361000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-004-0028-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,4]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2004,4]]}},"alternative-id":["10.1007\/s00165-004-0028-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-004-0028-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,4]]}}}