c © Springer-Verlag 2002 An assertional criterion for atomicity

Abstract. A criterion is presented to prove atomicity of read-write ob-jects by means of ghost variables and invariants. The criterion is applied to Bloom’s construction of a two-writer atomic register from two one-writer atomic registers and to the algorithm of Vitanyi and Awerbuch for the con-struction of a read-write object with m readers and writers, based on m2 read-write objects for one reader and one writer. In both cases, the proof comes down to the verification of a number of invariants. The hand-written proofs of these invariants have been verified with a mechanical theorem prover.