A challenge for atomicity verification

11 years 6 months ago
A challenge for atomicity verification
An unpublished algorithm of Haldar and Vidyasankar implements an atomic variable of an arbitrary type T for one writer and one reader by means of 4 unsafe variables of type T , three two-valued safe variables, and one three-valued regular variable. We present this algorithm, and prove its correctness by means of a refinement towards a known specification of an atomic variable. The refinement is a composition of refinement functions and a forward simulation. The correctness proof requires many nontrivial invariants. In its construction, we relied on the proof assistant PVS for the administration of invariants and proofs and the preservation of consistency. c 2008 Elsevier B.V. All rights reserved.
Wim H. Hesselink
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2008
Where SCP
Authors Wim H. Hesselink
Comments (0)