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.
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.
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.
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.
[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