A criterion for atomicity revisited

Concurrent and reactive programs are specified by their behaviours in the presence of a nondeterministic environment. In a natural way, this gives a specification (ARW) of an atomic variable. Several implementations of atomic variables by lower level primitives are known. A few years ago, we formulated a criterion to prove the correctness of such implementations. The proof of correctness of the criterion itself was based on a definition of atomicity by serialization points. Here, this criterion is reformulated as a specification HRW in the formal sense. Simulations from HRW to ARW and vice versa are constructed. These now serve as a constructive proof of correctness of the criterion. Eternity variables are used in the simulation from HRW to ARW. We propose so-called gliding simulations to deal with the problems that appear when occasionally the concrete implementation needs fewer steps than the abstract specification