ePrints

Metastability in Asynchronous Wait-Free Protocols

Lookup NU author(s): Dr Stephen Paynter, Neil Henderson, Dr James Armstrong

Downloads

• Published version [.pdf]

Abstract

Metastability can undermine the correctness of protocols which are demonstrably correct when metastability is ignored, e.g. when shared bits are assumed to be L(amport)-safe registers. We establish this using the CSP process algebra and the FDR2 model-checker, which we use to investigate 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. On the one hand, these ACMs exhibit different failure modes when metastability effects defeat hardware design measures to contain them. In this case the commonly used L-safe bit abstraction might rule out possible failure behaviours. On the other hand, most of these ACMs function correctly when metastability is resolved between instructions. In this case the L-safe abstraction permits failure behaviours which would not actually occur. Consequently, impossibility results concerning ACMs which are based on L-safe bit models may be pessimistic. We demonstrate this by showing that Simpson's 4-slot ACM functions correctly when constraints associated with metastability containment hold.

Publication metadata

Author(s): Paynter S, Henderson N, Armstrong JM

Publication type: Article

Publication status: Published

Journal: IEEE Transactions on Computers

Year: 2006

Volume: 55

Issue: 3

Pages: 292-303

Date deposited: 26/11/2004

ISSN (print): 0018-9340

ISSN (electronic): 1557-9956

Publisher: IEEE

URL: http://dx.doi.org/10.1109/TC.2006.42

DOI: 10.1109/TC.2006.42

Altmetrics

Share