Revisiting the Paxos Algorithm

De Prisco, Lampson and Lynch have studied the Paxos algorithm. 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 is not widely known or understood. In this work a new presentation of the Paxos algorithm, based on a formal decomposition into several interacting components, is provided. A correctness proof and a time performance and fault-tolerance analysis is also provided. The presentation is built upon a general timed automaton (GTA) model. The correctness proof uses automaton composition and invariant assertion methods. The time performance and fault-tolerance analysis is conditional on the stabilization of the underlying physical system behavior starting from some point in an execution. In order to formalize this stabilization, a special type of GTA called a Clock GTA is defined.

Roberto DePrisco, Butler Lampson, and Nancy Lynch. Revisiting the Paxos algorithm. In Marios Mavronicolas and Philippas Tsigas, editors, Proceedings of 11th International Workshop on Distributed Algorithms (WDAG'97, Saarbrucken, Germany, September 1997), volume 1320 of Lecture Notes in Computer Science, pages 111-125. Springer-Verlag 1997. .pdf

Also,

Roberto DePrisco,Butler Lampson, and Nancy Lynch. Fundamental study: Revisiting the Paxos algorithm. Theoretical Computer Science, 243:35--91, 2000.

TOC / LCS / MIT
Last modified: Wed February 14, 15:10 2001
Comments?