Proving atomicity: An assertional approach

Gregory Chockler, Nancy Lynch, Sayan Mitra, Joshua Tauber

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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. In addition, we show that a simplified version of our specification is implemented by a general atomic object construction based on the Lamport's replicated state machine algorithm.

Original languageEnglish (US)
Title of host publicationDistributed Computing - 19th International Conference, DISC 2005, Proceedings
Pages152-168
Number of pages17
DOIs
StatePublished - 2005
Externally publishedYes
Event19th International Conference on Distributed Computing, DISC 2005 - Cracow, Poland
Duration: Sep 26 2005Sep 29 2005

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3724 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other19th International Conference on Distributed Computing, DISC 2005
Country/TerritoryPoland
CityCracow
Period9/26/059/29/05

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Proving atomicity: An assertional approach'. Together they form a unique fingerprint.

Cite this