| Publication Title: |
Proving Atomicity: An Assertional Approach |
| Publication Author: |
Chockler, Gregory |
| Additional Authors: |
Nancy Lynch, Sayan Mitra, and Joshua Tauber |
| LCS Document Number: |
MIT-LCS-TR-995 |
| Publication Date: |
7-22-2005 |
| LCS Group: |
Theory of Computation |
| Additional URL: |
|
| Abstract: |
| 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 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
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 Attiya, Bar-Noy and Dolev, its
optimized version based on real time, and the shared memory register
construction of Vitanyi and Awerbuch), and by a general atomic
object implementation based on the Lamport\'s replicated state
machine algorithm. |
| To obtain this publication: |
|
|
|
To purchase a printed copy of this publication please contact
MIT
Document Services.
|