Synthesis of distributed algorithms with parameterized threshold guards

Marijana Lazić, Igor Konnov, Josef Widder, Roderick Bloem

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Fault-tolerant distributed algorithms are notoriously hard to get right. In this paper we introduce an automated method that helps in that process: the designer provides specifications (the problem to be solved) and a sketch of a distributed algorithm that keeps arithmetic details unspecified. Our tool then automatically fills the missing parts. Fault-tolerant distributed algorithms are typically parameterized, that is, they are designed to work for any number n of processes and any number t of faults, provided some resilience condition holds; e.g., n > 3t. In this paper we automatically synthesize distributed algorithms that work for all parameter values that satisfy the resilience condition. We focus on thresholdguarded distributed algorithms, where actions are taken only if a sufficiently large number of messages is received, e.g., more than t or n/2. Both expressions can be derived by choosing the right values for the coefficients a, b, and c, in the sketch of a threshold a·n+b·t+c. Our method takes as input a sketch of an asynchronous threshold-based fault-tolerant distributed algorithm-where the guards are missing exact coefficients-and then iteratively picks the values for the coefficients. Our approach combines recent progress in parameterized model checking of distributed algorithms with counterexample-guided synthesis. Besides theoretical results on termination of the synthesis procedure, we experimentally evaluate our method and show that it can synthesize several distributed algorithms from the literature, e.g., Byzantine reliable broadcast and Byzantine one-step consensus. In addition, for several new variations of safety and liveness specifications, our tool generates new distributed algorithms.

Original languageEnglish
Title of host publication21st International Conference on Principles of Distributed Systems, OPODIS 2017
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volume95
ISBN (Electronic)9783959770613
DOIs
Publication statusPublished - 1 Mar 2018
Event21st International Conference on Principles of Distributed Systems, OPODIS 2017 - Lisboa, Portugal
Duration: 18 Dec 201720 Dec 2017

Conference

Conference21st International Conference on Principles of Distributed Systems, OPODIS 2017
CountryPortugal
CityLisboa
Period18/12/1720/12/17

Keywords

  • Byzantine faults
  • Fault-tolerant distributed algorithms
  • Parameterized model checking
  • Program synthesis

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Synthesis of distributed algorithms with parameterized threshold guards'. Together they form a unique fingerprint.

  • Cite this

    Lazić, M., Konnov, I., Widder, J., & Bloem, R. (2018). Synthesis of distributed algorithms with parameterized threshold guards. In 21st International Conference on Principles of Distributed Systems, OPODIS 2017 (Vol. 95). [32] Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.OPODIS.2017.32