language: en

Revisiting the Paxos algorithm *

Roberto De Prisco a , Butler Lampson a, Nancy Lynch a
a MIT Laboratory for Computer Science
545 Technology Square NE43, Cambridge, MA 02139, USA.
Email: frobdep,lampson,lynchg@theory.lcs.mit.edu.

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

Keywords: I/O automata models, formal verification, distributed consensus, partially synchronous systems, fault-tolerance

1 Introduction