Model Checking of Consensus Algorithms

André Schiper
2006
Rapport ou document de travail

We show for the first time that standard model checking allows one to completely verify asynchronous algorithms for solving consensus, a fundamental problem in fault-tolerant distributed computing. Model checking is a powerful verification methodology based on state exploration. However it has rarely been applied to consensus algorithms, because these algorithms induce huge, often infinite state spaces. Here we focus on consensus algorithms based on the Heard-Of model (HO model, for short), a new computation model for distributed computing. By making use of the high abstraction level provided by this computation model, we develop a methodology for verifying consensus algorithms in every possible state by model checking. This paper describes the proposed verification methodology and the results of applying it to various consensus algorithms.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés

Chargement

Publications associées

Chargement

André Schiper
2006
Rapport ou document de travail

Résumé

Official source

https://infoscience.epfl.ch/record/97221?ln=fr

À propos de ce résultat

Concepts associés (10)

Concepts associés

Chargement

Publications associées (37)

Publications associées

Chargement

Problème du consensus

Le problème du consensus est un problème fondamental en théorie du calcul distribué. Il consiste pour un ensemble de machines à se mettre d'accord sur une valeur ou, par extension, sur une séquence de

Vérification de modèles

thumb|308x308px|Principe du model checking. En informatique, la vérification de modèles, ou model checking en anglais, est le problème suivant : vérifier si le modèle d'un système (souvent informatiqu

Tolérance aux pannes

vignette|Fichier GIF animé de 8 algorithmes ECT dans un réseau 802.1aq. La source est surlignée en violet, la destination en jaune. Les lignes violettes sont des chemins entre la source et la destinat

On The Weakest Failure Detector Ever

Rachid Guerraoui

Many problems in distributed computing are impossible when no information about process failures is available. So what is the minimal yet non-trivial failure information? In other words, what is the minimal information about failures needed to circumvent any impossibility and sufficient to circumvent some impossibility. This paper proposes a candidate abstraction, denoted ?, to capture this failure information. In every run of the distributed system, ? eventually informs the processes that some set of processes in the system cannot be the set of correct processes in that run. Although seemingly weak, for it might provide random information for an arbitrarily long period of time, and it only excludes one possibility of correct set among many, ? still captures non-trivial failure information. We show that ? is sufficient to circumvent the celebrated wait-free set-agreement impossibility. While doing so, we (a) disprove previous conjectures about the weakest failure detector to solve set-agreement and we (b) prove that solving set-agreement with registers is strictly weaker than solving n + 1-process consensus using n-process consensus. We prove that ? is, in some sense, necessary to circumvent any wait-free impossibility. As a corollary, set-agreement is, from a failure information perspective, a minimal wait-free impossible problem in distributed computing. Our results are generalized through an abstraction ?f that we introduce and prove necessary to solve any problem that cannot be solved in an f -resilient manner, and yet sufficient to solve f -resilient f -set-agreement.

2007

Chargement

The Time-Complexity of Local Decision in Distributed Agreement

Partha Dutta, Rachid Guerraoui, Bastian Pochon

Agreement is at the heart of distributed computing. In its simple form, it requires a set of processes to decide on a common value out of the values they propose. The time-complexity of distributed agreement problems is generally measured in terms of the number of communication rounds needed to achieve a global decision; i.e., for all non-faulty (correct) processes to reach a decision. This paper studies the time-complexity of local decisions in agreement problems, which we de¯ne as the number of communication rounds needed for at least one correct process to decide. We explore bounds for early local decision, that depend on the number f of actual failures (that occur in a given run of an algorithm), out of the maximum number t of failures tolerated (by the algorithm). We ¯rst consider the synchronous message-passing model where we give tight local decision bounds for three variants of agreement: consensus, uniform consensus and (non-blocking) atomic commit. We use these results to (1) show that, for consensus, local decision bounds are not compatible with global decision bounds (roughly speaking, they cannot be reached by the same algorithm), and (2) draw the ¯rst sharp line between the time-complexity of uniform consensus and atomic commit. Then we consider the eventually synchronous model where we give tight local decision bounds for synchronous runs of uniform consensus. (In this model, consensus and uniform consensus are similar, atomic commit is impossible, and one cannot bound the number of rounds to reach a decision in non-synchronous runs of consensus algorithms.) We prove a counter-intuitive result that the early local decision bound is the same as the early global decision bound. We also give a matching early deciding consensus algorithm that is signi¯cantly better than previous eventually synchronous consensus algorithms.

2007

Chargement

The Hidden Complexity of Distributed Systems

Karolos Antoniadis

The field of distributed computing has a long history, of more than fifty years. During that time, our understanding of the field has improved immensely and a certain body of folklore beliefs has formed. However, such folklore beliefs are not necessarily always true. In this thesis, we identify hidden complexities (in the sense of intricacies or costs) of distributed systems that contradict some of these folklore beliefs. Specifically, in this thesis, we challenge accepted beliefs in the following way: i) consensus algorithms need not be leader-based: there exists a deterministic leaderless consensus algorithm that is robust to non-synchronous periods, ii) completing a state machine replication command can be arbitrarily more expensive than solving a consensus instance, and iii) no data store actually provides fast transactions because they are impossible. Our results are associated to some of the fundamental problems in the field of distributed computing and are of significant practical relevance.

EPFL2020

Chargement