000112729 001__ 112729 000112729 005__ 20190509132133.0 000112729 0247_ $$2doi$$a10.5075/epfl-thesis-3980 000112729 02470 $$2urn$$aurn:nbn:ch:bel-epfl-thesis3980-4 000112729 02471 $$2nebis$$a5449835 000112729 037__ $$aTHESIS 000112729 041__ $$aeng 000112729 088__ $$a3980 000112729 245__ $$aA formal approach to fault tolerant distributed consensus 000112729 269__ $$a2008 000112729 260__ $$bEPFL$$c2008$$aLausanne 000112729 300__ $$a213 000112729 336__ $$aTheses 000112729 502__ $$aWan Fokkink, Rachid Guerraoui, Stephan Merz 000112729 520__ $$aThe term distributed Consensus denotes the problem of getting a certain number of processes, that could be far away from each other and that exchange messages through some communication means, to all agree on the same value. This problem has been proved impossible to solve in asynchronous settings when at least one process can crash, i.e., stop working. Since the problem of reaching Consensus among processes is recurrent in the domain of distributed computation, many algorithms have been proposed for solving it, circumventing the impossibility result through the introduction of some kind of synchrony in the system. Such algorithms are traditionally expressed in natural language or in pseudocode, thus sometimes generating ambiguities on their contents and on their correctness proofs. In this thesis, we propose a simple, yet efficient way of providing formal descriptions and proofs of distributed Consensus algorithms. Such method is based on the use of inference rules, it requires very little prior knowledge in order to be understood, and follows closely the way algorithms are expressed in pseudocode, thus being intuitive for the users. To show the validity of our claims, we use our method to formalize two of the major distributed Consensus algorithms, namely the Chandra-Toueg and the Paxos algorithms. Using our rigorous description, we then formally prove that such algorithms guarantee the respect of the Validity, Agreement and Termination properties that every solution to the Consensus problem should provide. This proving exercise actually reveals interesting results. We see that the Chandra-Toueg and the Paxos algorithms have strong points of resemblance and their correctness proofs can be carried out in very similar manners. However, while the Chandra-Toueg algorithm proves to be correct under the point of view of the three properties, we discover that Paxos does not give any guarantee of terminating. This generates a philosophical question: should such algorithm be considered a Consensus algorithm or not? 000112729 6531_ $$aformal methods, distributed algorithms 000112729 6531_ $$adistributed consensus 000112729 6531_ $$atransition systems 000112729 6531_ $$acorrectness proofs 000112729 6531_ $$atermination 000112729 700__ $$0(EPFLAUTH)148002$$g148002$$aFuzzati, Rachele 000112729 720_2 $$aNestmann, Uwe$$edir. 000112729 720_2 $$aSchiper, André$$edir.$$g106377$$0241767 000112729 8564_ $$uhttps://infoscience.epfl.ch/record/112729/files/EPFL_TH3980.pdf$$zTexte intégral / Full text$$s1422624$$yTexte intégral / Full text 000112729 909C0 $$xU10409$$0252187$$pLAMP 000112729 909C0 $$xU10411$$0252206$$pLSR 000112729 909CO $$ooai:infoscience.tind.io:112729$$qDOI2$$qGLOBAL_SET$$pthesis$$pthesis-bn2018$$pDOI$$pIC 000112729 918__ $$dEDHP$$bIC-SIN$$cIIF$$aIC 000112729 919__ $$aLAMP1 000112729 919__ $$aLSR 000112729 920__ $$b2008$$a2008-3-10 000112729 970__ $$a3980/THESES 000112729 973__ $$sPUBLISHED$$aEPFL 000112729 980__ $$aTHESIS