Author(s): Paynter, S. E., Henderson N. and Armstrong, J. M.
Abstact: 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 with Lamport-safe models of bits; furthermore, realistic bit models can demonstrate protocols correct which Lamport-safe bit models would suggest were incorrect.