Safety-Liveness Exclusion in Distributed Computing

Victor Bushkov, Rachid Guerraoui
ACM Press, 2015
Rapport ou document de travail

The history of distributed computing is full of trade-offs between safety and liveness. For instance, one of the most celebrated results in the field, namely the impossibility of consensus in an asynchronous system basically says that we cannot devise an algorithm that deterministically ensures consensus agreement and validity (i.e., safety) on the one hand, and consensus wait-freedom (i.e., liveness) on the other hand. The motivation of this work is to study the extent to which safety and liveness properties inherently exclude each other. More specifically, we ask, given any safety property S, whether we can determine the strongest (resp. weakest) liveness property that can (resp. cannot) be achieved with S. We show that, maybe surprisingly, the answers to these safety-liveness exclusion questions are in general negative. This has several ramifications in various distributed computing contexts. In the context of consensus for example, this means that it is impossible to determine the strongest (resp. the weakest) liveness property that can (resp. cannot) be ensured with linearizability. However, we present a way to circumvent these impossibilities and answer positively the safety-liveness question by considering a restricted form of liveness. We consider a definition that gathers generalized forms of obstruction-freedom and lock-freedom while enabling to determine the strongest (resp. weakest) liveness property that can (resp. cannot) be implemented in the context of consensus and transactional memory.

À 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

Victor Bushkov, Rachid Guerraoui
ACM Press, 2015
Rapport ou document de travail

Résumé

Official source

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

À propos de ce résultat

Concepts associés (7)

Concepts associés

Chargement

Publications associées (35)

Publications associées

Chargement

Transactional memory

In computer science and engineering, transactional memory attempts to simplify concurrent programming by allowing a group of load and store instructions to execute in an atomic way. It is a concurrenc

Computing

Computing is any goal-oriented activity requiring, benefiting from, or creating computing machinery. It includes the study and experimentation of algorithmic processes, and developm

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

Safety-Liveness Exclusion in Distributed Computing

Victor Bushkov, Rachid Guerraoui

ACM2015

Chargement

Model Checking of Consensus Algorithms

André Schiper

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.

2006

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