License
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://drops.dagstuhl.de/opus/volltexte/2018/8635/
Go to the corresponding LIPIcs Volume Portal


Lazic, Marijana ; Konnov, Igor ; Widder, Josef ; Bloem, Roderick

Synthesis of Distributed Algorithms with Parameterized Threshold Guards

pdf-format:
LIPIcs-OPODIS-2017-32.pdf (0.7 MB)


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
Seminar: 21st International Conference on Principles of Distributed Systems (OPODIS 2017)
Issue Date: 2018
Date of publication: 16.03.2018


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI