MIT-LCS-TR-995 Proving Atomicity: An Assertional Approach

Abstract. Atomicity (or linearizability) is a commonly used consistency criterion for distributed services and objects. Although atomic object im-plementations are abundant, proving that algorithms achieve atomicity has turned out to be a challenging problem. In this paper, we initiate the study of systematic ways of verifying distributed implementations of atomic objects, beginning with read/write objects (registers). Our general approach is to replace the existing operational reasoning about events and partial orders with assertional reasoning about invariants and simulation relations. To this end, we define an abstract state machine that captures the atomicity property and prove correctness of the object implementations by establishing a simulation mapping between the im-plementation and the specification automata. We demonstrate the gen-erality of our specification by showing that it is implemented by three different read/write register constructions: the message-passing register emulation of Attiya, Bar-Noy and Dolev, its optimized version based on real time, and the shared memory register construction of Vitanyi and Awerbuch. In addition, we show that a simplified version of our specifi-cation is implemented by a general atomic object construction based on the Lamport’s replicated state machine algorithm.