Synthesis of distributed algorithms with parameterized threshold guards

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

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem Konferenzband

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.

Originalspracheenglisch
Titel21st International Conference on Principles of Distributed Systems, OPODIS 2017
Herausgeber (Verlag)Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Band95
ISBN (elektronisch)9783959770613
DOIs
PublikationsstatusVeröffentlicht - 1 Mär 2018
Veranstaltung21st International Conference on Principles of Distributed Systems, OPODIS 2017 - Lisboa, Portugal
Dauer: 18 Dez 201720 Dez 2017

Konferenz

Konferenz21st International Conference on Principles of Distributed Systems, OPODIS 2017
LandPortugal
OrtLisboa
Zeitraum18/12/1720/12/17

ASJC Scopus subject areas

  • Software

Fingerprint

Untersuchen Sie die Forschungsthemen von „Synthesis of distributed algorithms with parameterized threshold guards“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren