puter Science 243 (2000) 35 – 91 ate/tcs Fundamental Study Revisiting the PAXOS algorithm * Roberto De Prisco a,*, Butler Lampson b, Nancy Lynch a a MIT Laboratory puter Science, 545 Technology Square, Cambridge, MA 02139, USA b Microsoft Corporation, 180 Lake View Ave, Cambridge, MA 02138, USA Received October 1998; revised July municated by M. Mavronicolas Abstract The PAXOS algorithm is an efficient and highly fault-tolerant algorithm, devised by Lamport, for reaching consensus ina 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 position into several ponents. 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 isa notion of“ normal ” timing behavior, but that do not necessarily always exhibit this “ normal ” timing behavior. ~c 2000 Elsevier Science . All rights reserved. Keywords: I/O automata models; Formal verification; Distributed consensus; Partially synchronous systems; Fault-tolerance Contents 1. Introduction...............................................................................................36 . Related work.........................................................................................38 . Road map............................................................................................39 0. Model s................................................................................................. ...39 . I/O automata and the GTA..........................................................................39 . The Clock GTA.....................................................................................40 . Composition of automat
Revisiting the PAXOS algorithm 来自淘豆网m.daumloan.com转载请标明出处.
