A proof technique for register atomicity: Preliminary version

Baruch Awerbuch, Lefteris M. Kirousis, Evangelos Kranakis, Paul M.B. Vitányi

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


An implementation of a concurrent data object is wait-free if any process can complete any operation in a bounded number of steps, independently of the execution speeds of the programs. Much recent work has been done on concurrent access of shared variables by asynchronous processes. That work shows that implementing such shared variables does not require synchronization (by e.g. mutual exclusion), but can be solved in a wait-free manner. A fruitful paradigm in this context is the notion of a shared register satisfying a niceness condition called atomicity. Recent proposed solutions have led to the realization that: (1) neither the problem to be solved nor the model required were rigorously defined, (2) there was no clear insight in what constitutes a good proof of correctness in the area, and (3) the proposed protocols are so complicated that although correctness may be possible in a "platonic fashion", verifiability seems impossible to attain by human beings. A lot of controversy and allegations about constructions and proofs have arisen. Consequently, we have spent great effort to put the area on a rigorous basis. The thrust of this paper is to provide a new proof technique, and demonstrate its applicability by a non-trivial example. In other words, a new model is rigorously presented for the first time, and then a new method is given for proving register atomicity. It is then used to give a simple proof of the atomicity of the first and only direct construction of a multireader multiwriter register from atomic 1-reader 1-writer registers. (This construction was given in [8], by two of the present authors, with a completely different proof.)

Original languageEnglish (US)
Title of host publicationFoundations of Software Technology and Theoretical Computer Science - 8th Conference, Proceedings
EditorsKesav V. Nori, Sanjeev Kumar
PublisherSpringer Verlag
Number of pages18
ISBN (Print)9783540505174
StatePublished - 1988
Event8th International Conference on Foundations of Software Technology and Theoretical Computer Science, FST and TCS 1988 - Pune, India
Duration: Dec 21 1988Dec 23 1988

Publication series

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


Conference8th International Conference on Foundations of Software Technology and Theoretical Computer Science, FST and TCS 1988

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'A proof technique for register atomicity: Preliminary version'. Together they form a unique fingerprint.

Cite this