Communication-closed asynchronous protocols

Abstract : Fault-tolerant distributed systems are implemented over asyn-chronous networks, so that they use algorithms for asynchronous models with faults. Due to asynchronous communication and the occurrence of faults (e.g., process crashes or the network dropping messages) the implementations are hard to understand and analyze. In contrast, synchronous computation models simplify design and reasoning. In this paper, we bridge the gap between these two worlds. For a class of asynchronous protocols, we introduce a procedure that, given an asynchronous protocol , soundly computes its round-based synchronous counterpart. This class is defined by properties of the sequential code. We computed the synchronous counterpart of known consensus and leader election protocols, such as, Paxos, and Chandra and Toueg's consensus. Using Verifast we checked the sequential properties required by the rewriting. We verified the round-based synchronous counterpart of Multi-Paxos, and other algorithms, using existing deductive verification methods for synchronous protocols.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [45 references]  Display  Hide  Download

https://hal.inria.fr/hal-01991415
Contributor : Cezara Dragoi <>
Submitted on : Wednesday, January 23, 2019 - 6:54:19 PM
Last modification on : Wednesday, January 30, 2019 - 11:07:51 AM

File

head2.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01991415, version 1

Collections

Citation

Andrei Damian, Cezara Dragoi, Alexandru Militaru, Josef Widder. Communication-closed asynchronous protocols. 2019. ⟨hal-01991415⟩

Share

Metrics

Record views

189

Files downloads

157