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