{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:37:17Z","timestamp":1725511037560},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2013,11,1]],"date-time":"2013-11-01T00:00:00Z","timestamp":1383264000000},"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":[[2013,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Simpson and Harris have described multi-slot algorithms implementing a single-place buffer, each operating without explicit hardware synchronisation mechanisms. Conventional refinement and proof techniques have explained\n            <jats:italic>that<\/jats:italic>\n            these algorithms work, but do not give convincing descriptions of\n            <jats:italic>how<\/jats:italic>\n            they work. An unconventional refinement process starting from the classic single-variable buffer, using both data and atomicity refinement and drawing information from unsuccessful steps, derives each algorithm. The logic used is RGSep, a marriage of rely\/guarantee and concurrent separation logic. Extensive detailed verifications are described. The result is an explanation of how the algorithms work and some pointers to how such algorithms might be devised.\n          <\/jats:p>","DOI":"10.1007\/s00165-011-0213-4","type":"journal-article","created":{"date-parts":[[2011,12,8]],"date-time":"2011-12-08T13:47:58Z","timestamp":1323352078000},"page":"893-931","source":"Crossref","is-referenced-by-count":10,"title":["Explanation of two non-blocking shared-variable communication algorithms"],"prefix":"10.1145","volume":"25","author":[{"given":"Richard","family":"Bornat","sequence":"first","affiliation":[{"name":"Department of Engineering and Information Sciences, Middlesex University, NW4 4BT, London, UK"}]},{"given":"Hasan","family":"Amjad","sequence":"additional","affiliation":[{"name":"Department of Engineering and Information Sciences, Middlesex University, NW4 4BT, London, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Abrial J-R (2008) Formal development of Simpson\u2019s 4-slot algorithm. Private communication July 2008"},{"key":"e_1_2_1_2_2_2","unstructured":"Abrial J-R Cansell D (2006) Formal development of Simpson\u2019s 4-slot algorithm. Private communication March 2006"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Alglave J Fox A Ishtiaq S Myreen MO Sarkar S Sewell P Zappa Nardelli F (2009) The semantics of Power and ARM multiprocessor machine code. In: DAMP 2009: workshop on declarative aspects of multicore programming January 2009","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0141-8"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3472-0","volume-title":"The origin of concurrent programming","author":"Brinch Hansen P","year":"2002"},{"key":"e_1_2_1_2_6_2","unstructured":"Dijkstra EW (1965) Cooperating sequential processes. Technical report EWD-123 Technical University Eindhoven. Reprinted in [Gen68] and [Bri02]"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Floyd RW (1967) Assigning meanings to programs. In: Schwartz JT (ed) Mathematical aspects of computer science. Proceedings of symposia in applied mathematics vol 19 Providence Rhode Island. American Mathematical Society pp 19\u201332","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_2_8_2","unstructured":"Genuys F (ed) (1968) Programming languages. Academic Press"},{"key":"e_1_2_1_2_9_2","unstructured":"Harris T (2004) A non-blocking three-slot buffer. Private communication; described in [BA10]"},{"key":"e_1_2_1_2_10_2","first-page":"244","volume-title":"FME Lecture notes in computer science vol 2805.","author":"Henderson N","year":"2003"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/114005.102808"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Henderson N Paynter S (2002) The formal classification and verification of Simpson\u2019s 4-slot asynchronous communication mechanism. In: FME 2002: Formal methods\u2014getting IT right. Lecture notes in computer science vol 2391. Springer Berlin pp 121\u2013132","DOI":"10.1007\/3-540-45614-7_20"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_2_14_2","unstructured":"Jones CB (1983) Specification and design of (parallel) programs. In: IFIP Congress pp 321\u2013332"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Jones CB Pierce KG (2008) Splitting atoms with rely\/guarantee conditions coupled with data reification. In: ABZ \u201908: Proceedings of the 1st international conference on abstract state machines B and Z. Springer Berlin pp 360\u2013377","DOI":"10.1007\/978-3-540-87603-8_47"},{"key":"e_1_2_1_2_16_2","unstructured":"Jones CB Pierce KG (2009) Elucidating concurrent algorithms via layers of abstraction and reification. Technical report CS-TR-1166 Newcastle University Computing Science"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Lakatos I (1976) Proofs and refutations: the logic of mathematical discovery. Cambridge University Press","DOI":"10.1017\/CBO9781139171472"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Owens S Sarkar S Sewell P (2009) A better x86 memory model: x86-TSO. In: TPHOLs 2009: theorem proving in higher order logics. LNCS vol. 5674 pp 391\u2013407","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_2_1_2_20_2","first-page":"478","volume-title":"ECOOP 2010\u2014object-oriented programming 24th European conference Lecture notes in computer science vol 6183.","author":"Owens S","year":"2010"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-004-0042-9"},{"key":"e_1_2_1_2_22_2","unstructured":"Rushby J (2002) Model checking Simpson\u2019s four-slot fully asynchronous communication mechanism. Technical report Computer Science Laboratory SRI International"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1986.0018"},{"issue":"1","key":"e_1_2_1_2_24_2","first-page":"17","article-title":"Four-slot fully asynchronous communication mechanism","volume":"137","author":"Simpson HR","year":"1990","journal-title":"IEE Proc"},{"issue":"1","key":"e_1_2_1_2_25_2","first-page":"35","article-title":"Correctness analysis for class of asynchronous communication mechanisms","volume":"139","author":"Simpson HR","year":"1992","journal-title":"IEE Proc"},{"issue":"227","key":"e_1_2_1_2_26_2","first-page":"144, 227","article-title":"New algorithms for asynchronous communication","volume":"144","author":"Simpson HR","year":"1997","journal-title":"IEE Proc: Comput Digital Tech"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1049\/ip-cdt:19971219"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/22.4.332"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Sarkar S Sewell P Alglave J Maranget L Williams D (2011) Understanding POWER multiprocessors. In: Proc. PLDI","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Sarkar S Sewell P Zappa Nardelli F Owens S Ridge T Braibant T Myreen M Alglave J (2009) The semantics of x86-CC multiprocessor machine code. In: Proc. POPL 2009 January 2009","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_2_1_2_32_2","unstructured":"Vafeiadis V (2007) Modular fine-grained concurrency verification. PhD thesis University of Cambridge"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Vafeiadis V Parkinson MJ (2007) A marriage of rely\/guarantee and separation logic. In: CONCUR 2007\u2014concurrency theory. LNCS vol 4037 pp 256\u2013271 August 2007","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0213-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0213-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0213-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:55:04Z","timestamp":1641484504000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0213-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":34,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["10.1007\/s00165-011-0213-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0213-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,11]]}}}