License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.OPODIS.2017.32
URN: urn:nbn:de:0030-drops-86359
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8635/
Lazic, Marijana ;
Konnov, Igor ;
Widder, Josef ;
Bloem, Roderick
Synthesis of Distributed Algorithms with Parameterized Threshold Guards
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 threshold- guarded 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 algo- rithms with counterexample-guided synthesis. Besides theoretical results on termination of the synthesis procedure, we experimentally evaluate our method and show that it can synthesize sev- eral 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.
BibTeX - Entry
@InProceedings{lazic_et_al:LIPIcs:2018:8635,
author = {Marijana Lazic and Igor Konnov and Josef Widder and Roderick Bloem},
title = {{Synthesis of Distributed Algorithms with Parameterized Threshold Guards}},
booktitle = {21st International Conference on Principles of Distributed Systems (OPODIS 2017)},
pages = {32:1--32:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-061-3},
ISSN = {1868-8969},
year = {2018},
volume = {95},
editor = {James Aspnes and Alysson Bessani and Pascal Felber and Jo{\~a}o Leit{\~a}o},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/8635},
URN = {urn:nbn:de:0030-drops-86359},
doi = {10.4230/LIPIcs.OPODIS.2017.32},
annote = {Keywords: fault-tolerant distributed algorithms, byzantine faults, parameterized model checking, program synthesis}
}
|
Keywords: |
|
fault-tolerant distributed algorithms, byzantine faults, parameterized model checking, program synthesis |
|
Collection: |
|
21st International Conference on Principles of Distributed Systems (OPODIS 2017) |
|
Issue Date: |
|
2018 |
|
Date of publication: |
|
28.03.2018 |
