*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] New AFP entry: Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 30 Jul 2012 12:41:26 +0200*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:14.0) Gecko/20120713 Thunderbird/14.0

Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model Henri Debrat and Stephan Merz Distributed computing is inherently based on replication, promising increased tolerance to failures of individual computing nodes or communication channels. Realizing this promise, however, involves quite subtle algorithmic mechanisms, and requires precise statements about the kinds and numbers of faults that an algorithm tolerates (such as process crashes, communication faults or corrupted values). The landmark theorem due to Fischer, Lynch, and Paterson shows that it is impossible to achieve Consensus among N asynchronously communicating nodes in the presence of even a single permanent failure. Existing solutions must rely on assumptions of "partial synchrony". Indeed, there have been numerous misunderstandings on what exactly a given algorithm is supposed to realize in what kinds of environments. Moreover, the abundance of subtly different computational models complicates comparisons between different algorithms. Charron-Bost and Schiper introduced the Heard-Of model for representing algorithms and failure assumptions in a uniform framework, simplifying comparisons between algorithms. In this contribution, we represent the Heard-Of model in Isabelle/HOL. We define two semantics of runs of algorithms with different unit of atomicity and relate these through a reduction theorem that allows us to verify algorithms in the coarse-grained semantics (where proofs are easier) and infer their correctness for the fine-grained one (which corresponds to actual executions). We instantiate the framework by verifying six Consensus algorithms that differ in the underlying algorithmic mechanisms and the kinds of faults they tolerate. http://afp.sourceforge.net/entries/Heard_Of.shtml Thanks to the authors, and enjoy!

- Previous by Date: Re: [isabelle] Fun vs Primrec: difference?
- Next by Date: [isabelle] Redundant trace with jEdit
- Previous by Thread: Re: [isabelle] Is this overloading?
- Next by Thread: [isabelle] Redundant trace with jEdit
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list