Document Open Access Logo

Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries

Authors Nathalie Bertrand , Igor Konnov , Marijana Lazić , Josef Widder

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.33.pdf
  • Filesize: 0.71 MB
  • 15 pages

Document Identifiers

Author Details

Nathalie Bertrand
  • Univ. Rennes, Inria, CNRS, IRISA, Rennes, France
Igor Konnov
  • University of Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France
Marijana Lazić
  • TU München, 85748 Garching bei München, Germany
Josef Widder
  • TU Wien, 1040 Vienna, Austria
  • Interchain Foundation, 6340 Baar, Switzerland

Funding

Supported by the Austrian Science Fund (FWF) via the National Research Network RiSE (S11403, S11405), project PRAVDA (P27722), and Doctoral College LogiCS (W1255-N23); by the Vienna Science and Technology Fund (WWTF) via project APALACHE (ICT15-103); and by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS). Experiments presented in this paper were carried out using the Grid'5000 testbed, supported by a scientific interest group hosted by Inria and including CNRS, RENATER, and others, see https://www.grid5000.fr.

Cite AsGet BibTex

Nathalie Bertrand, Igor Konnov, Marijana Lazić, and Josef Widder. Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.33

Abstract

Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round r-1. For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or’s and Bracha’s seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
  • Software and its engineering → Software fault tolerance
  • Theory of computation → Logic and verification
Keywords
  • threshold automata
  • counter systems
  • parameterized verification
  • randomized distributed algorithms
  • Byzantine faults

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Marcos Aguilera and Sam Toueg. The correctness proof of Ben-Or’s randomized consensus algorithm. Distributed Computing, pages 1-11, 2012. online first. Google Scholar
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. Michael Ben-Or. Another Advantage of Free Choice: Completely Asynchronous Agreement Protocols (Extended Abstract). In PODC, pages 27-30, 1983. Google Scholar
  4. Nathalie Bertrand and Paulin Fournier. Parameterized Verification of Many Identical Probabilistic Timed Processes. In FSTTCS, volume 24 of LIPIcs, pages 501-513, 2013. Google Scholar
  5. Gabriel Bracha. Asynchronous Byzantine Agreement Protocols. Inf. Comput., 75(2):130-143, 1987. Google Scholar
  6. Mouna Chaouch-Saad, Bernadette Charron-Bost, and Stephan Merz. A Reduction Theorem for the Verification of Round-Based Distributed Algorithms. In RP, volume 5797 of LNCS, pages 93-106, 2009. Google Scholar
  7. Andrei Damian, Cezara Drăgoi, Alexandru Militaru, and Josef Widder. Communication-closed asynchronous protocols. In CAV, 2019. (to appear). Google Scholar
  8. Tzilla Elrad and Nissim Francez. Decomposition of Distributed Programs into Communication-Closed Layers. Sci. Comput. Program., 2(3):155-173, 1982. Google Scholar
  9. Michael J. Fischer, Nancy A. Lynch, and M. S. Paterson. Impossibility of Distributed Consensus with one Faulty Process. J. ACM, 32(2):374-382, 1985. Google Scholar
  10. Igor Konnov, Marijana Lazić, Helmut Veith, and Josef Widder. A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms. In POPL, pages 719-734, 2017. Google Scholar
  11. Igor Konnov, Marijana Lazic, Helmut Veith, and Josef Widder. Para²: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms. Formal Methods in System Design, 51(2):270-307, 2017. Google Scholar
  12. Igor Konnov, Helmut Veith, and Josef Widder. On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability. Information and Computation, 252:95-109, 2017. Google Scholar
  13. Igor Konnov and Josef Widder. ByMC: Byzantine model checker. In ISoLA (3), volume 11246 of LNCS, pages 327-342. Springer, 2018. Google Scholar
  14. Jure Kukovec, Igor Konnov, and Josef Widder. Reachability in Parameterized Systems: All Flavors of Threshold Automata. In CONCUR, pages 19:1-19:17, 2018. Google Scholar
  15. Marta Z. Kwiatkowska and Gethin Norman. Verifying Randomized Byzantine Agreement. In FORTE, pages 194-209, 2002. Google Scholar
  16. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In CAV, pages 585-591, 2011. Google Scholar
  17. Marta Z. Kwiatkowska, Gethin Norman, and Roberto Segala. Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM. In CAV, pages 194-206, 2001. Google Scholar
  18. Daniel J. Lehmann and Michael O. Rabin. On the Advantages of Free Choice: A Symmetric and Fully Distributed Solution to the Dining Philosophers Problem. In POPL, pages 133-138, 1981. Google Scholar
  19. Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, and Philipp Rümmer. Fair Termination for Parameterized Probabilistic Concurrent Systems. In TACAS, volume 10205 of LNCS, pages 499-517, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_29.
  20. Anthony Widjaja Lin and Philipp Rümmer. Liveness of Randomised Parameterised Systems under Arbitrary Schedulers. In CAV, volume 9780 of LNCS, pages 112-133. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_7.
  21. Achour Mostéfaoui, Hamouma Moumen, and Michel Raynal. Randomized k-set agreement in crash-prone and Byzantine asynchronous systems. Theor. Comput. Sci., 709:80-97, 2018. Google Scholar
  22. Amir Pnueli and Lenore D. Zuck. Verification of Multiprocess Probabilistic Protocols. Distributed Computing, 1(1):53-72, 1986. URL: https://doi.org/10.1007/BF01843570.
  23. Yee Jiun Song and Robbert van Renesse. Bosco: One-Step Byzantine Asynchronous Consensus. In DISC, volume 5218 of LNCS, pages 438-450, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact