This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Metastability in Asynchronous Wait-Free Protocols
March 2006 (vol. 55 no. 3)
pp. 292-303
We demonstrate that the safe register abstraction is an inappropriate model of a shared bit variable in an ACM. This is due to the phenomenon of metastability and the way that circuits are engineered to reduce the probability of it propagating. We give a bit model that takes the engineered restrictions into account and which is therefore stronger than the safe bit model. With our bit model we show that some impossibility results concerning ACMs which are based on safe bit models are pessimistic. We establish this using the CSP process algebra and the FDR2 model-checker, by investigating the impact of various models of shared bits on different wait-free protocols, including Lamport's regular register, Simpson's 4-slot ACM, Kirousis et al.'s ACM, Tromp's Atomic Bit and 4-Track ACMs, and Haldar and Subramanian's ACM. We show how these protocols can fail in the presence of rereadable metastability.

[1] G.L. Peterson, “Concurrent Reading while Writing,” ACM Trans. Programming Languages and Systems, vol. 5, no. 1, pp. 46-55, Jan. 1983.
[2] L. Lamport, “On Interprocess Communication— Part 2: Algorithms,” Distributed Computing, vol. 1, pp. 86-101, 1986.
[3] H. Simpson, “Four-Slot Fully Asynchronous Communication Mechanism,” IEE Proc., vol. 137 Part E, no. 1, pp. 17-30, Jan. 1990.
[4] M.B. Josephs, C. Hoare, and H. Jifeng, “A Theory of Asynchronous Processes,” Technical Report PRG-TR-6-89, Programming Research Group, Oxford Univ. Computing Laboratory, Feb. 1989.
[5] C. Hoare, “Monitors: An Operating System Structuring Concept,” Comm. ACM, vol. 17, no. 10, pp. 549-557, 1974.
[6] R. Männer, “Metastable States in Asynchronous Digital Systems: Avoidable or Unavoidable?” Microelectronic Reliability, vol. 28, no. 2, pp. 295-307, 1988.
[7] S. Paynter, N. Henderson, and J. Armstrong, “Ramifications of Metastability in Bit Variables Explored via Simpson's 4-Slot Mechanism,” Formal Aspects of Computing, vol. 16, no. 4, pp. 332-351, Nov. 2004.
[8] H. Simpson, “Fully Asynchronous Communication,” Proc. IEE Colloquium MASCOT in Real-Time Systems, May 1987.
[9] L. Kirousis, E. Kranakis, and P. Vitányi, “Atomic Multireader Register,” Proc. Workshop Distributed Algorithms, pp. 278-296, 1987.
[10] J. Tromp, “How to Construct an Atomic Variable (Extended Abstract),” Proc. Third Int'l Workshop Distributed Algorithms, pp. 292-302, 1989.
[11] S. Haldar and P. Subramanian, “Space-Optimum Conflict-Free Construction of Buffer-Optimal 1-Writer 1-Reader Multivalued Atomic Variable,” Proc. Eighth Int'l Workshop Distributed Algorithms (WDAG '94), pp. 116-129, 1994.
[12] D.J. Kinniment, A. Bystrov, and A.V. Yakovlev, “Synchronization Circuit Performance,” IEEE J. Solid-State Circuits, vol. 37, no. 2, pp. 202-209, 2002.
[13] T.J. Chaney and C.E. Molnar, “Anomalous Behavior of Synchronizer and Arbitor Circuits,” IEEE Trans. Computers, vol. 22, no. 4, pp. 421-422, Apr. 1973.
[14] J.U. Horstmann, H.W. Eichek, and R.L. Coates, “Metastability Behaviour of CMOS ASIC Flip-Flops in Theory and Test,” IEEE J. Solid-State Circuits, vol. 24, no. 1, pp. 146-157, Feb. 1989.
[15] J. Kessels, “Register-Communication Between Mutually Asynchronous Domains,” Proc. 11th Int'l Symp. Asynchronous Circuits and Systems (ASYNC '05), 2005.
[16] L.R. Marino, “General Theory of Metastable Operation,” IEEE Trans. Computers, vol. 30, no. 2, pp. 107-115, Feb. 1981.
[17] L. Kleeman and A. Cantoni, “On the Unavoidability of Metastable Behaviour in Digital Systems,” IEEE Trans. Computers, vol. 36, no. 1, pp. 109-112, Jan. 1987.
[18] D.M. Chapiro, “Reliable High-Speed Arbitration and Synchronization,” IEEE Trans. Computers, vol. 36, no. 10, pp. 1251-1255, Oct. 1987.
[19] R. Ginosar, “Fourteen Ways to Fool Your Synchronizer,” Proc. 11th Int'l Symp. Asynchronous Circuit and Systems (ASYNC '03), pp. 89-95, 2003.
[20] N. Henderson and S. Paynter, “The Formal Classification and Verification of Simpson's 4-Slot Asynchronous Communication Mechanism,” Proc. 11 Int'l Symp. Formal Methods Europe (FME '02), L.-H. Eriksson and P. Lindsay, eds., pp. 350-369, 2002.
[21] S. Haldar and K. Vidyasankar, “Buffer-Optimal Constructions of 1-Writer Multireader Multivalued Atomic Shared Variables,” J. Parallel and Distributed Computing, vol. 31, pp. 174-180, 1995.
[22] J.E. Burns and G.L. Peterson, “The Ambiguity of Choosing,” Proc. Eighth Ann. Symp. Principles of Distributed Computing (PODC '89), pp. 145-157, 1989.
[23] S. Haldar and K. Vidyasankar, “Space-Optimal Buffer-Based Conflict-Free Construction of 1-Writer 1-Reader Multivalued Atomic Variables from Safe Bits,” unpublished paper, 2001.
[24] A. Roscoe, The Theory and Practice of Concurrency. Prentice Hall Series in Computer Science, 1998.
[25] I. Clark, F. Xia, A. Yakovlev, and A. Davis, “Petri Net Models of Latch Metastability,” Electronic Letters, vol. 34, no. 7, pp. 635-636, 1998.
[26] I. Clark, “A Unified Approach to the Study of Asynchronous Communication Mechansims in Real-Time Systems,” PhD dissertation, London Univ., King's College, May 2000.
[27] Failures-Divergence Refinement: The FDR 2.0 User Manual. Formal Systems (Europe) Ltd., Aug. 1996.
[28] H. Simpson, “Correctness Analysis for Class of Asynchronous Communication Mechanism,” IEE Proc., vol. 139 Part E, no. 1, pp. 35-49, Jan. 1992.
[29] H. Simpson, “Role Model Analysis of an Asynchronous Communication Mechanism,” IEE Proc. Computers and Digital Techniques, vol. 144, no. 4, pp. 232-240, July 1997.
[30] P. Brooke, J.L. Jacob, and J.M. Armstrong, “Analysis of the Four-Slot Mechanism,” Proc. BCS-FACS Northern Formal Methods Workshop, 1996.
[31] P. Brooke, “A Timed Semantics for a Hierarchical Design Notation,” PhD dissertation, Dept. of Computer Science, Univ. of York, Apr. 1999.
[32] F. Xia and I. Clark, “Complementing the Role Model Method with Petri Net Techniques in Studying Issues of Data Freshness of the Four-Slot Mechanism,” Hardware Design and Petri-Nets, pp. 33-50, Kluwer Academic, 2000.
[33] F. Xia, “Supporting the MASCOT Method with Petri Net Techniques for Real-Time Systems Development,” PhD dissertation, London Univ., King's College, Jan. 2000.
[34] J. Rushby, “Model-Checking Simpson's Four-Slot Fully Asychronous Communication Mechanism,” technical report, Computer Science Laboratory— SRI Int'l, July 2002.
[35] N. Henderson, “Proving the Correctness of Simpson's 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method,” FM 2003: The 12th Int'l Formal Methods Europe Symp., 2003.
[36] N. Henderson, “The Formal Modelling and Analysis of an Asynchronous Communication Mechanism,” PhD dissertation, School of Computing Science, Univ. of Newcastle upon Tyne, Feb. 2005.

Index Terms:
Protocol verification, model checking, formal models, asynchronous operation.
Citation:
Stephen E. Paynter, Neil Henderson, James M. Armstrong, "Metastability in Asynchronous Wait-Free Protocols," IEEE Transactions on Computers, vol. 55, no. 3, pp. 292-303, March 2006, doi:10.1109/TC.2006.42
Usage of this product signifies your acceptance of the Terms of Use.