Document Open Access Logo

Characterizing Consensus in the Heard-Of Model

Authors A. R. Balasubramanian, Igor Walukiewicz

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.9.pdf
  • Filesize: 0.86 MB
  • 18 pages

Document Identifiers

Author Details

A. R. Balasubramanian
  • Technical University of Munich, Germany
Igor Walukiewicz
  • CNRS, LaBRI, University of Bordeaux, France

Funding

  • Balasubramanian, A. R.: UMI ReLaX, ERC Advanced Grant 787367 (PaVeS).
  • Walukiewicz, Igor: ANR FREDDA ANR-17-CE40-0013.

Cite AsGet BibTex

A. R. Balasubramanian and Igor Walukiewicz. Characterizing Consensus in the Heard-Of Model. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.9

Abstract

The Heard-Of model is a simple and relatively expressive model of distributed computation. Because of this, it has gained a considerable attention of the verification community. We give a characterization of all algorithms solving consensus in a fragment of this model. The fragment is big enough to cover many prominent consensus algorithms. The characterization is purely syntactic: it is expressed in terms of some conditions on the text of the algorithm.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Software and its engineering → Software verification
  • Theory of computation → Logic and verification
Keywords
  • consensus problem
  • Heard-Of model
  • verification

Metrics

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

Related Versions

References

  1. Marcos K. Aguilera, Carole Delporte-Gallet, Hugues Fauconnier, and Sam Toueg. Partial synchrony based on set timeliness. Distributed Computing, 25(3):249-260, 2012. URL: https://doi.org/10.1007/s00446-012-0158-8.
  2. Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, and Florian Zuleger. Parameterized model checking of synchronous distributed algorithms by abstraction. In Isil Dillig and Jens Palsberg, editors, Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, volume 10747 of Lecture Notes in Computer Science, pages 1-24. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-73721-8_1.
  3. A.R. Balasubramanian and Igor Walukiewicz. Characterizing consensus in the heard-of model. URL: http://arxiv.org/abs/2004.09621.
  4. Nathalie Bertrand, Igor Konnov, Marijana Lazic, and Josef Widder. Verification of randomized consensus algorithms under round-rigid adversaries. In Wan Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, volume 140 of LIPIcs, pages 33:1-33:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.33.
  5. Martin Biely, Josef Widder, Bernadette Charron-Bost, Antoine Gaillard, Martin Hutle, and André Schiper. Tolerating corrupted communication. In Indranil Gupta and Roger Wattenhofer, editors, Proceedings of the Twenty-Sixth Annual ACM Symposium on Principles of Distributed Computing, PODC 2007, pages 244-253. ACM, 2007. URL: https://doi.org/10.1145/1281100.1281136.
  6. Tushar Deepak Chandra, Vassos Hadzilacos, and Sam Toueg. The weakest failure detector for solving consensus. J. ACM, 43(4):685-722, 1996. URL: https://doi.org/10.1145/234533.234549.
  7. Tushar Deepak Chandra and Sam Toueg. Unreliable failure detectors for reliable distributed systems. J. ACM, 43(2):225-267, 1996. URL: https://doi.org/10.1145/226643.226647.
  8. Mouna Chaouch-Saad, Bernadette Charron-Bost, and Stephan Merz. A reduction theorem for the verification of round-based distributed algorithms. In Olivier Bournez and Igor Potapov, editors, Reachability Problems, 3rd International Workshop, RP 2009, volume 5797 of Lecture Notes in Computer Science, pages 93-106. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04420-5_10.
  9. Bernadette Charron-Bost, Henri Debrat, and Stephan Merz. Formal verification of consensus algorithms tolerating malicious faults. In Xavier Défago, Franck Petit, and Vincent Villain, editors, Stabilization, Safety, and Security of Distributed Systems - 13th International Symposium, SSS 2011, volume 6976 of Lecture Notes in Computer Science, pages 120-134. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24550-3_11.
  10. Bernadette Charron-Bost and Stephan Merz. Formal verification of a consensus algorithm in the heard-of model. Int. J. Software and Informatics, 3(2-3):273-303, 2009. URL: http://www.ijsi.org/ch/reader/view_abstract.aspx?file_no=273&flag=1.
  11. Bernadette Charron-Bost and André Schiper. The heard-of model: computing in distributed systems with benign faults. Distributed Computing, 22(1):49-71, 2009. Google Scholar
  12. Flaviu Cristian and Christof Fetzer. The timed asynchronous distributed system model. IEEE Trans. Parallel Distrib. Syst., 10(6):642-657, 1999. URL: https://doi.org/10.1109/71.774912.
  13. Andrei Damian, Cezara Dragoi, Alexandru Militaru, and Josef Widder. Communication-closed asynchronous protocols. In CAV (2), volume 11562 of Lecture Notes in Computer Science, pages 344-363. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_20.
  14. Henri Debrat and Stephan Merz. Verifying fault-tolerant distributed algorithms in the heard-of model. Archive of Formal Proofs, 2012, 2012. URL: https://www.isa-afp.org/entries/Heard_Of.shtml.
  15. Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. A logic-based framework for verifying consensus algorithms. In Kenneth L. McMillan and Xavier Rival, editors, Verification, Model Checking, and Abstract Interpretation VMCAI 2014, volume 8318 of Lecture Notes in Computer Science, pages 161-181. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54013-4_10.
  16. Cezara Dragoi, Thomas A. Henzinger, and Damien Zufferey. Psync: a partially synchronous language for fault-tolerant distributed algorithms. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pages 400-415. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837650.
  17. Cynthia Dwork, Nancy A. Lynch, and Larry J. Stockmeyer. Consensus in the presence of partial synchrony. J. ACM, 35(2):288-323, 1988. URL: https://doi.org/10.1145/42282.42283.
  18. Michael J. Fischer, Nancy A. Lynch, and Mike Paterson. Impossibility of distributed consensus with one faulty process. J. ACM, 32(2):374-382, 1985. URL: https://doi.org/10.1145/3149.214121.
  19. Felix C. Freiling, Rachid Guerraoui, and Petr Kuznetsov. The failure detector abstraction. ACM Comput. Surv., 43(2):9:1-9:40, 2011. URL: https://doi.org/10.1145/1883612.1883616.
  20. Eli Gafni. Round-by-round fault detectors: Unifying synchrony and asynchrony (extended abstract). In Brian A. Coan and Yehuda Afek, editors, Proceedings of the Seventeenth Annual ACM Symposium on Principles of Distributed Computing, PODC '98, pages 143-152. ACM, 1998. URL: https://doi.org/10.1145/277697.277724.
  21. Rachid Guerraoui and Michel Raynal. The alpha of indulgent consensus. Comput. J., 50(1):53-67, 2007. URL: https://doi.org/10.1093/comjnl/bxl046.
  22. Michel Hurfin, Achour Mostéfaoui, and Michel Raynal. A versatile family of consensus protocols based on chandra-toueg’s unreliable failure detectors. IEEE Trans. Computers, 51(4):395-408, 2002. URL: https://doi.org/10.1109/12.995450.
  23. Igor Konnov, Helmut Veith, and Josef Widder. SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, volume 9206 of Lecture Notes in Computer Science, pages 85-102. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_6.
  24. Igor V. Konnov, Marijana Lazic, Helmut Veith, and Josef Widder. A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 719-734. ACM, 2017. URL: http://dl.acm.org/citation.cfm?id=3009860.
  25. Igor V. Konnov, Helmut Veith, and Josef Widder. On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Inf. Comput., 252:95-109, 2017. URL: https://doi.org/10.1016/j.ic.2016.03.006.
  26. Jure Kukovec, Igor Konnov, and Josef Widder. Reachability in parameterized systems: All flavors of threshold automata. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, volume 118 of LIPIcs, pages 19:1-19:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.19.
  27. Ognjen Maric. Formal Verification of Fault-Tolerant Systems. PhD thesis, ETH Zurich, 2017. Google Scholar
  28. Ognjen Maric, Christoph Sprenger, and David A. Basin. Cutoff bounds for consensus algorithms. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, volume 10427 of Lecture Notes in Computer Science, pages 217-237. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_12.
  29. Yoram Moses. Knowledge in distributed systems. In Encyclopedia of Algorithms, pages 1051-1055. Springer, 2016. URL: https://doi.org/10.1007/978-1-4939-2864-4_606.
  30. Yoram Moses and Sergio Rajsbaum. A layered analysis of consensus. SIAM J. Comput., 31(4):989-1021, 2002. URL: https://doi.org/10.1137/S0097539799364006.
  31. Achour Mostéfaoui and Michel Raynal. Solving consensus using chandra-toueg’s unreliable failure detectors: A general quorum-based approach. In Prasad Jayanti, editor, Distributed Computing, 13th International Symposium, volume 1693 of Lecture Notes in Computer Science, pages 49-63. Springer, 1999. URL: https://doi.org/10.1007/3-540-48169-9_4.
  32. Michel Raynal and Julien Stainer. Synchrony weakened by message adversaries vs asynchrony restricted by failure detectors. In Panagiota Fatourou and Gadi Taubenfeld, editors, ACM Symposium on Principles of Distributed Computing, PODC '13, pages 166-175. ACM, 2013. URL: https://doi.org/10.1145/2484239.2484249.
  33. Olivier Rütti, Zarko Milosevic, and André Schiper. Generic construction of consensus algorithms for benign and byzantine faults. In Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010, pages 343-352. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/DSN.2010.5544299.
  34. Yee Jiun Song, Robbert van Renesse, Fred B. Schneider, and Danny Dolev. The building blocks of consensus. In Shrisha Rao, Mainak Chatterjee, Prasad Jayanti, C. Siva Ram Murthy, and Sanjoy Kumar Saha, editors, Distributed Computing and Networking, 9th International Conference, ICDCN 2008, volume 4904 of Lecture Notes in Computer Science, pages 54-72. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-77444-0_5.
  35. Ilina Stoilkovska, Igor Konnov, Josef Widder, and Florian Zuleger. Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. In Tomás Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, volume 11428 of Lecture Notes in Computer Science, pages 357-374. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17465-1_20.
  36. Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. Modularity for decidability of deductive verification with applications to distributed systems. In Jeffrey S. Foster and Dan Grossman, editors, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pages 662-677. ACM, 2018. URL: https://doi.org/10.1145/3192366.3192414.
  37. Tatsuhiro Tsuchiya and André Schiper. Verification of consensus algorithms using satisfiability solving. Distributed Computing, 23(5-6):341-358, 2011. URL: https://doi.org/10.1007/s00446-010-0123-3.
  38. Robbert van Renesse, Nicolas Schiper, and Fred B. Schneider. Vive la différence: Paxos vs. viewstamped replication vs. zab. IEEE Trans. Dependable Sec. Comput., 12(4):472-484, 2015. URL: https://doi.org/10.1109/TDSC.2014.2355848.
  39. Klaus von Gleissenthall, Nikolaj Bjørner, and Andrey Rybalchenko. Cardinalities and universal quantifiers for verifying parameterized systems. In Chandra Krintz and Emery Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, pages 599-613. ACM, 2016. URL: https://doi.org/10.1145/2908080.2908129.
  40. Josef Widder and Ulrich Schmid. The theta-model: achieving synchrony without clocks. Distributed Computing, 22(1):29-47, 2009. URL: https://doi.org/10.1007/s00446-009-0080-x.
  41. James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas E. Anderson. Verdi: a framework for implementing and formally verifying distributed systems. In David Grove and Steve Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 357-368. ACM, 2015. URL: https://doi.org/10.1145/2737924.2737958.
  42. Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas E. Anderson. Planning for change in a formal verification of the raft consensus protocol. In Jeremy Avigad and Adam Chlipala, editors, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pages 154-165. ACM, 2016. URL: https://doi.org/10.1145/2854065.2854081.
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