2026-07-21T20:03:14Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:8635 2024-03-06T10:42:14Z ddc:004 open_access

Synthesis of Distributed Algorithms with Parameterized Threshold Guards Lazic, Marijana Konnov, Igor Widder, Josef Bloem, Roderick fault-tolerant distributed algorithms byzantine faults parameterized model checking program synthesis 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Marijana Lazic and Igor Konnov and Josef Widder and Roderick Bloem 2018 Is Part Of LIPIcs, Volume 95, 21st International Conference on Principles of Distributed Systems (OPODIS 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.OPODIS.2017.32 urn:nbn:de:0030-drops-86359 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2017.32 eng https://creativecommons.org/licenses/by/3.0/legalcode