A Unified Framework for Specifying and Proving Atomicity

Gregory Chockler, Nancy Lynch, Sayan Mitra, Joshua Tauber

Introduction

Many distributed and network-based services can be modeled as shared objects accessible to (possibly remote) clients through a well-defined interface. Atomicity is a desirable property for such objects as it allows the object operations invoked in each particular run to be perceived as occurring atomically in some sequential order.

Although atomic object implementations are abundant, proving that an implementation satisfies atomicity turns out to be challenging. The existing proof methods are based on reasoning about events and their ordering and as a result, are prone to subtle errors. As an evidence to that effect, several published shared memory read/write atomic object implementations were later shown to be bogus even though they were accompanied by what seemed to be rigorous proofs.

Approach
We propose to develop a unified formal framework for proving atomicity of the shared object implementations. The main part of the framework is an operational specification of an abstract protocol (called a Partial Order machine, or PO) that orders operations gradually, by first constructing a partial order and then extending it to the final total order. The implementation correctness is then proved by showing that it simulates the abstract specification.

We intend to use the I/O Automata (IOA) [7] framework as our implementation and specification formalisms. The IOA framework provides a rigorous mathematical foundation for reasoning about the implementation algorithms and their correctness. It also allows us to benefit from the IOA code generator to automatically translate our implementations to executable Java programs, and to verify our proofs' logic by using the PVS theorem prover augmented with the IOA library.

Progress
The specification of PO machine has been completed and proved correct. We implemented the message-passing atomic object emulation algorithm by Attiya, Bar-Noy and Dolev (ABD) [2] and proved it correct by exhibiting a forward simulation from ABD to PO. To further demonstrate generality and utility of our specification, we implemented a time-based optimization of the ABD protocol (using the Timed IOA model [3]) and showed its correctness can still be proven by simulating the PO machine. We also used PO to show correctness of the Vitanyi and Awerbuch [9] algorithm that constructs a multi-writer/multi-reader atomic object from single-writer/single-reader objects.

We used the IOA code generator to produce executable Java programs for our ABD implementation. We successfully ran the generated code on a cluster of workstations and conducted some performance experiments. We are currently working on verifying our proofs using the PVS theorem prover.

Future Work
We will aim to implement more atomic object algorithms and show their correctness using the PO machine. Our next objective is to depart from the world of read/write objects and focus on proving correctness of arbitrarily typed object implementations. In particular, we are going to focus on implementing and proving correctness of an atomic object implementation based on the Lamport's replicated state machine (RSM) algorithm [4].

Another objective is to demonstrate that our specifications are easily customizable to obtain weaker consistency guarantees, such as regular [6], safe [6], multi-writer regular [8], sequentially consistent (serializable) [5], etc. We intend to show how to use customized specifications to prove correctness of Byzantine register constructions [1].

Finally, we will aim to substantiate the claim that our framework encompasses most of the existing read/write object constructions found in the literature. To demonstrate this point, we will show how our framework can be used to prove safety of several constructions from the literature. Although our framework is clearly applicable to timestamp-based register constructions, it is still unclear whether it can be used for constructions that order operations implicitly (e.g., by using hand-shaking mechanisms). In our future research we will seek to answer this question.

References
[1] Ittai Abraham, Gregory Chockler, Idit Keidar and Dahlia Malkhi. Byzantine Disk Paxos: Optimal Resilience with Byzantine Shared Memory. In Proceedings of the 23rd Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC 2004) July 25-28, 2004, St. John's, Newfoundland, Canada

[2] H. Attiya, A. Bar-Noy and D. Dolev, Sharing Memory Robustly in Message-Passing Systems, Journal of the ACM, Vol. 42, No. 1 (January 1995), pp. 124--142.

[3] Dilsun Kirli Kaynar, Nancy Lynch, Roberto Segala, and Frits Vaandrager. Timed I/O Automata: A Mathematical Framework for Modeling and Analyzing Real-Time Systems. RTSS 2003: The 24th IEEE International Real-Time Systems Symposium, Cancun, Mexico, December, 2003.

[4] L. Lamport. Time, Clocks and the Ordering of Events in a Distributed System Communications of the ACM 21, 7 (July 1978), 558-565.

[5] L. Lamport. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Transactions on Computers C-28, 9 (September 1979) 690-691

[6] L. Lamport. On Interprocess Communication--Part I: Basic Formalism, Part II: Algorithms. Distributed Computing 1, 2 (1986), 77-101

[7] Nancy Lynch and Mark Tuttle. An Introduction to Input/Output automata. CWI-Quarterly, 2(3):219--246, September 1989. Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands. Also, Technical Memo MIT/LCS/TM-373, Laboratory for Computer Science, Massa

[8] Cheng Shao, Evelyn Pierce, Jennifer L. Welch: Multi-writer Consistency Conditions for Shared Memory Objects. DISC 2003: 106-120

[9] P.M.B. Vitanyi and B. Awerbuch, Atomic shared register access by asynchronous hardware, Proceedings 27th Annual IEEE Symposium on Foundations of Computer Science, 1986, 233-243