Roberto de Prisco, Butler Lampson, and Nancy Lynch
Citation: Theoretical Computer Science 243, 1-2 (July 2000), pp 35-91. A preliminary version appeared as Proc. WDAG'97, Lecture Notes in Computer Science 1320, Springer, 1997, pp 111-125.
Links: Abstract, Acrobat. Here is an HTML version created by OCR for the benefit of search engines; it is not meant for human consumption.
Email: blampson@microsoft.com. This paper is at http://research.microsoft.com.
Abstract:
The Paxos algorithm is an efficient and highly fault-tolerant algorithm, devised by Lamport, for reaching consensus in a distributed system. Although it appears to be practical, it seems to be not widely known or understood. This paper contains a new presentation of the PAXOS algorithm, based on a formal decomposition into several interacting components. It also contains a correctness proof and a time performance and fault-tolerance analysis. The formal framework used for the presentation of the algorithm is provided by the Clock General Timed Automaton (Clock GTA) model. The Clock GTA provides a systematic way of describing timing-based systems in which there is a notion of \normal" timing behavior, but that do not necessarily always exhibit this \normal" timing behavior.