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.
Also, Roberto DePrisco,Butler Lampson, and Nancy Lynch. |

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