Distributed Consensus, revisited

We provide a novel model to formalize a well-known algorithm, by Chandra and Toueg, that solves Consensus among asynchronous distributed processes in the presence of a particular class of failure detectors (3S or, equivalently, Ω), under the hypothesis that only a minority of processes may crash. The model is defined as a global transition system that is unambigously generated by local transition rules. The model is syntax-free in that it does not refer to any form of programming language or pseudo code. We use our model to formally prove that the algorithm is correct.

• Type: Journal
• Year: 2007
• Where: ACTA
• Authors: Rachele Fuzzati, Massimo Merro, Uwe Nestmann
• Keywords: ACTA 2007, Asynchronous Distributed Processes, Model, Well-known Algorithm