Proving Atomicity: An Assertional Approach

9 years 11 months ago
Proving Atomicity: An Assertional Approach
Atomicity (or linearizability) is a commonly used consistency criterion for distributed services and objects. Although atomic object implementations 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 on 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 implementation and the specification automata. We demonstrate the generality of our specification by showing that it is implemented by three different read/write register constructions: the message-passing register emulation of Attiy...
Gregory Chockler, Nancy A. Lynch, Sayan Mitra, Jos
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where WDAG
Authors Gregory Chockler, Nancy A. Lynch, Sayan Mitra, Joshua A. Tauber
Comments (0)