Revisiting the PAXOS algorithm

The PAXOS algorithm is an efficient and highly fault-tolerant algorithm, de vised 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 f ormal 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 provide s a systematic way of describing timing-based systems in which there is a n otion of "normal" timing behavior, but that do not necessarily always exhib it this "normal" timing behavior. (C) 2000 Elsevier Science B.V. All rights reserved.