112729
20190509132133.0
doi
10.5075/epfl-thesis-3980
urn
urn:nbn:ch:bel-epfl-thesis3980-4
nebis
5449835
THESIS
eng
3980
A formal approach to fault tolerant distributed consensus
2008
Lausanne
EPFL
2008
213
Theses
Wan Fokkink, Rachid Guerraoui, Stephan Merz
The 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?
formal methods, distributed algorithms
distributed consensus
transition systems
correctness proofs
termination
(EPFLAUTH)148002
Fuzzati, Rachele
148002
Nestmann, Uwe
dir.
241767
Schiper, André
dir.
106377
1422624
http://infoscience.epfl.ch/record/112729/files/EPFL_TH3980.pdf
Texte intégral / Full text
Texte intégral / Full text
252187
LAMP
U10409
252206
LSR
U10411
oai:infoscience.tind.io:112729
thesis
thesis-bn2018
DOI
IC
DOI2
GLOBAL_SET
IC
IC-SIN
IIF
EDHP
LAMP1
LSR
2008-3-10
2008
3980/THESES
EPFL
PUBLISHED
THESIS