Ramifications of metastability in bit variables explored via Simpson’s 4-slot mechanism
Stephen E. Paynter, N. Henderson, James M. Armstrong · Formal Aspects of Computing · 2004
Abstract. 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’s 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.