Revisiting the Paxos Algorithm
Citation: Proc. WDAG'97, Lecture Notes in Computer Science 1320, Springer, 1997, pp 111-125. A revised version appeared in Theoretical Computer Science 243, 1-2 (July 2000), pp 35-91 [63a].
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.