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. © 2000 Elsevier Science B.V. All rights reserved.
CITATION STYLE
De Prisco, R., Lampson, B., & Lynch, N. (2000). Revisiting the PAXOS algorithm. Theoretical Computer Science, 243(1–2), 35–91. https://doi.org/10.1016/s0304-3975(00)00042-6
Mendeley helps you to discover research relevant for your work.