{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:35:34Z","timestamp":1694622934652},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2004,11,1]],"date-time":"2004-11-01T00:00:00Z","timestamp":1099267200000},"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,11]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>Protocol descriptions often fail to take metastability into account. Metastability, however, can undermine protocols which depend on shared bits. In this paper a series of increasingly realistic models of bits are developed in CSP to explore the implications of metastability for Simpson\u2019s 4-slot asynchronous communication mechanism. It is shown that the 4-slot mechanism with realistic bit models preserves data-coherence, freshness, and sequencing, and is Lamport-atomic. We demonstrate that metastability can undermine the correctness of protocols demonstrated correct on the assumption that bits are Lamport-safe; furthermore, realistic bit models can demonstrate that protocols are correct which Lamport-safe bit models would suggest were incorrect or impossible.<\/jats:p>","DOI":"10.1007\/s00165-004-0042-9","type":"journal-article","created":{"date-parts":[[2004,5,24]],"date-time":"2004-05-24T05:48:43Z","timestamp":1085377723000},"page":"332-351","source":"Crossref","is-referenced-by-count":7,"title":["Ramifications of metastability in bit variables explored via Simpson\u2019s 4-slot mechanism"],"prefix":"10.1145","volume":"16","author":[{"given":"S. E.","family":"Paynter","sequence":"first","affiliation":[{"name":"MBDA UK Ltd., 5, BS34 7QW, Bristol, Filton, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N.","family":"Henderson","sequence":"additional","affiliation":[{"name":"BAE SYSTEMS, Dependable Computing Systems Centre, University of Newcastle, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. M.","family":"Armstrong","sequence":"additional","affiliation":[{"name":"Centre for Software Reliability, University of Newcastle, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"issue":"3","key":"p_1","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/BF01212305","article-title":"A criterion for atomicity","volume":"4","author":"Anderson James H.","year":"1992","journal-title":"Formal Aspects Comput"},{"key":"p_2","volume-title":"Proceedings of the BCS-FACS Northern Formal Methods Workshop","author":"Brooke Phillip","year":"1996"},{"key":"p_3","first-page":"145","volume-title":"8th annual symposium on principles of distributed computing (PODC'89)","author":"Burns James E.","year":"1989"},{"issue":"10","key":"p_5","doi-asserted-by":"crossref","first-page":"1251","DOI":"10.1109\/TC.1987.1676867","article-title":"Reliable high-speed arbitration and synchronization","volume":"36","author":"Chapiro Daniel M.","year":"1987","journal-title":"IEEE Trans Comput"},{"issue":"4","key":"p_7","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1109\/T-C.1973.223730","article-title":"Anomalous behavior of synchronizer and arbitor circuits","volume":"22","author":"Chaney Thomas J.","year":"1973","journal-title":"IEEE Trans Comput"},{"issue":"7","key":"p_8","doi-asserted-by":"crossref","first-page":"635","DOI":"10.1049\/el:19980502","article-title":"Petri net models of latch metastability","volume":"34","author":"Clark IG","year":"1998","journal-title":"Electron Lett"},{"key":"p_9","volume-title":"Failures-Divergence Refinement: The FDR 2.0 User Manual","author":"Ltd Formal Systems","year":"1996"},{"key":"p_10","first-page":"89","volume-title":"Proceedings of ASYNC'03","author":"Ginosar Ran","year":"2003"},{"issue":"1","key":"p_11","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1109\/4.16314","article-title":"Metastability behaviour of CMOS asic flip-flops in theory and test","volume":"24","author":"Horstmann Jens U.","year":"1989","journal-title":"IEEE J Solid-State Circuits"},{"key":"p_12","volume-title":"FM 2003: The 12th international FME symposium, lecture notes in computer science. Springer, Berlin Heidelberg New York","author":"Henderson","year":"2003"},{"issue":"10","key":"p_13","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1145\/355620.361161","article-title":"Monitors: an operating system structuring concept","volume":"17","author":"Hoare","year":"1974","journal-title":"Commun ACM"},{"key":"p_14","volume-title":"Communicating sequential processes","author":"Hoare","year":"1985"},{"key":"p_15","series-title":"Lecture Notes in computer Science","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1007\/3-540-45614-7_20","volume-title":"Eriksson L-H, Lindsay PA (eds) Proceedings of FME'02","author":"Henderson","year":"2002"},{"key":"p_16","volume-title":"Proceedings of 8th international workshop on distributed algorithms (WDAG'94)","volume":"839","author":"Haldar","year":"1994"},{"key":"p_17","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1006\/jpdc.1995.1156","article-title":"Buffer-optimal constructions of 1-writer multireader multivalued atomic shared variables","volume":"31","author":"Haldar","year":"1995","journal-title":"J Parallel Distributed Comput"},{"key":"p_18","volume-title":"Space-optimal buffer-based conflict-free construction of 1-writer 1-reader multivalued atomic variables from safe bits. Unpublished Paper","author":"Haldar","year":"2001"},{"key":"p_19","volume-title":"Programming research group","author":"Josephs Mark B.","year":"1989"},{"issue":"2","key":"p_20","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1109\/4.982426","article-title":"Synchronization circuit performance","volume":"37","author":"Kinniment David J.","year":"2002","journal-title":"IEEE J Solid-State Circuits"},{"issue":"1","key":"p_21","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1109\/TC.1987.5009455","article-title":"On the unavoidability of metastable behaviour in digital systems","volume":"36","author":"Kleeman Lindsay","year":"1987","journal-title":"IEEE Trans Comput"},{"key":"p_22","first-page":"278","volume-title":"Proceedings of the workshop on distributed algorithms. Lecture notes on computer science","author":"Kirousis LM","year":"1987"},{"key":"p_23","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BF01786227","article-title":"On interprocess communication - part 1: basic formalism","volume":"1","author":"Lamport","year":"1986","journal-title":"Distributed Comput"},{"key":"p_24","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/BF01786228","article-title":"On interprocess communication - part 2: algorithms","volume":"1","author":"Lamport","year":"1986","journal-title":"Distributed Comput"},{"issue":"2","key":"p_25","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/0026-2714(88)90363-0","article-title":"Metastable states in asynchronous digital systems: avoidable or unavoidable","volume":"28","author":"M\u00e4nner Reinhard","year":"1988","journal-title":"Microelectronic Reliability"},{"issue":"2","key":"p_26","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/TC.1981.6312173","article-title":"General theory of metastable operation","volume":"30","author":"Marino Leonard R.","year":"1981","journal-title":"IEEE Trans Comput"},{"issue":"1","key":"p_27","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1145\/357195.357198","article-title":"Concurrent reading while writing","volume":"5","author":"Peterson Gary L.","year":"1983","journal-title":"ACM Trans Programming Lang Syst"},{"key":"p_28","volume-title":"The theory and practice of concurrency","author":"Roscoe","year":"1998"},{"key":"p_29","volume-title":"Computer Science Laboratory - SRI International","author":"Rushby John","year":"2002"},{"key":"p_30","volume-title":"Proceedings of the IEE Colloquium on MASCOT in Real-Time Systems","author":"Simpson","year":"1987"},{"key":"p_31","volume-title":"IEE Proc 137 E(1):17-30","author":"Simpson","year":"1990"},{"key":"p_32","volume-title":"IEE Proc 139 E(1):35-49","author":"Simpson","year":"1992"},{"issue":"4","key":"p_33","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1049\/ip-cdt:19971218","article-title":"New algorithms for asynchronous communication","volume":"144","author":"Simpson","year":"1997","journal-title":"IEEE Proc Comput Digital Tech."},{"issue":"4","key":"p_34","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1049\/ip-cdt:19971219","article-title":"Role model analysis of an asynchronous communication mechanism","volume":"144","author":"Simpson","year":"1997","journal-title":"IEEE Proc Comput Digital Techniques"},{"issue":"3","key":"p_35","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1049\/ip-cdt:20030419","article-title":"Protocols for process interaction","volume":"150","author":"Simpson","year":"2003","journal-title":"IEEE Proc Comput Digital Tech."},{"issue":"2","key":"p_36","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1049\/ip-cdt:20040071","article-title":"Freshness specification for a class of asynchronous communication mechanisms","volume":"151","author":"Simpson","year":"2004","journal-title":"IEEE Proc Comput Digital Tech."},{"key":"p_37","series-title":"Lecture Notes in computer science","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/3-540-51687-5_51","volume-title":"Bermond J, Raynal M (eds) Proceedings of the 3rd international workshop on distributed algorithms","author":"Tromp John","year":"1989"},{"key":"p_38","volume-title":"Matra BAe Dynamics","author":"White","year":"2001"},{"key":"p_39","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/978-1-4757-3143-9_2","volume-title":"Hardware design and petri-nets","author":"Xia","year":"2000"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-004-0042-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-004-0042-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-004-0042-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:46:07Z","timestamp":1641483967000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-004-0042-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,11]]},"references-count":37,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,11]]}},"alternative-id":["10.1007\/s00165-004-0042-9"],"URL":"https:\/\/doi.org\/10.1007\/s00165-004-0042-9","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,11]]}}}