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 systema...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2005
|
| Online Access: | http://hdl.handle.net/1721.1/30559 |
| _version_ | 1826208170137092096 |
|---|---|
| author | Chockler, Gregory Lynch, Nancy Mitra, Sayan Tauber, Joshua |
| author2 | Theory of Computation |
| author_facet | Theory of Computation Chockler, Gregory Lynch, Nancy Mitra, Sayan Tauber, Joshua |
| author_sort | Chockler, Gregory |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T14:01:38Z |
| id | mit-1721.1/30559 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T14:01:38Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/305592019-04-12T08:26:07Z Proving Atomicity: An Assertional Approach Chockler, Gregory Lynch, Nancy Mitra, Sayan Tauber, Joshua Theory of Computation 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. 2005-12-22T02:33:34Z 2005-12-22T02:33:34Z 2005-07-22 MIT-CSAIL-TR-2005-048 MIT-LCS-TR-995 http://hdl.handle.net/1721.1/30559 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 15 p. 14829213 bytes 699536 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Chockler, Gregory Lynch, Nancy Mitra, Sayan Tauber, Joshua Proving Atomicity: An Assertional Approach |
| title | Proving Atomicity: An Assertional Approach |
| title_full | Proving Atomicity: An Assertional Approach |
| title_fullStr | Proving Atomicity: An Assertional Approach |
| title_full_unstemmed | Proving Atomicity: An Assertional Approach |
| title_short | Proving Atomicity: An Assertional Approach |
| title_sort | proving atomicity an assertional approach |
| url | http://hdl.handle.net/1721.1/30559 |
| work_keys_str_mv | AT chocklergregory provingatomicityanassertionalapproach AT lynchnancy provingatomicityanassertionalapproach AT mitrasayan provingatomicityanassertionalapproach AT tauberjoshua provingatomicityanassertionalapproach |