A challenge for atomicity verification

Hesselink, W. H., 1-Mar-2008, In : Science of computer programming. 71, 1, p. 57-72 16 p.

Research output: Contribution to journalArticleAcademicpeer-review

Copy link to clipboard



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.

Original languageEnglish
Pages (from-to)57-72
Number of pages16
JournalScience of computer programming
Issue number1
Publication statusPublished - 1-Mar-2008


  • atomicity, safe variables, regular variables, refinement, theorem proving, CRITERION

Download statistics

No data available

ID: 2756020