Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms
Distributed algorithms typically run over arbitrary many processes and may involve unboundedly many rounds, making the automated verification of their correctness challenging. Building on domain theory, we introduce a framework that abstracts infinite-state distributed systems that represent distributed algorithms into finite-state guard automata. The soundness of the approach corresponds to the Scott-continuity of the abstraction, which relies on the assumption that the distributed algorithms are layered. Guard automata thus enable the verification of safety and liveness properties of distributed algorithms.
Verification
Distributed algorithms
Domain theory
Theory of computation~Verification by model checking
Theory of computation~Distributed algorithms
15:1-15:17
Regular Paper
This project has received funding from Interchain Foundation (Switzerland).
https://hal.inria.fr/hal-03283388
Nathalie
Bertrand
Nathalie Bertrand
Université Rennes, Inria, CNRS, IRISA, France
https://orcid.org/0000-0002-9957-5394
Bastien
Thomas
Bastien Thomas
Université Rennes, Inria, CNRS, IRISA, France
Josef
Widder
Josef Widder
Informal Systems, Wien, Austria
https://orcid.org/0000-0003-2795-611X
10.4230/LIPIcs.CONCUR.2021.15
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Zeinab Ganjei, Ahmed Rezine, and Yunyun Zhu. Verification of cache coherence protocols wrt. trace filters. In Proceedings of the 15th International Conference on Formal Methods in Computer-Aided Design (FMCAD'15), pages 9-16. IEEE, 2015.
Samson Abramsky and Achim Jung. Domain Theory, volume 3 of Handbook of Logic in Computer Science, pages 1-168. Clarendon Press, 1994.
C. Aiswarya, Benedikt Bollig, and Paul Gastin. An automata-theoretic approach to the verification of distributed algorithms. Information and Computation, 259:305-327, 2018.
Francesco Alberti, Silvio Ghilardi, and Elena Pagani. Counting constraints in flat array fragments. In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR'16), volume 9706 of Lecture Notes in Computer Science, pages 65-81, 2016.
A. R. Balasubramanian, Javier Esparza, and Marijana Lazić. Complexity of verification and synthesis of threshold automata. In Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA'20), volume 12302 of Lecture Notes in Computer Science, pages 144-160. Springer, 2020.
Michael Ben-Or. Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract). In Proceedings of the 2nd Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC'83), pages 27-30, 1983.
Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, and Sharon Shoham. Verification of threshold-based distributed algorithms by decomposition to decidable logics. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV'19), volume 11562 of Lecture Notes in Computer Science, pages 245-266. Springer, 2019.
Piotr Berman and Juan A. Garay. Cloture votes: n/4-resilient distributed consensus in t+1 rounds. Mathematical Systems Theory, 26(1):3-19, 1993.
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015.
Luca Bortolussi and Jane Hillston. Model checking single agent behaviours by fluid approximation. Information and Computation, 242:183-226, 2015.
Gabriel Bracha and Sam Toueg. Asynchronous consensus and broadcast protocols. Journal of the ACM, 32(4):824-840, 1985.
Mouna Chaouch-Saad, Bernadette Charron-Bost, and Stephan Merz. A reduction theorem for the verification of round-based distributed algorithms. In Proceedings of the 3rd International Workshop on Reachability Problems (RP'09), volume 5797 of Lecture Notes in Computer Science, pages 93-106, 2009.
Bernadette Charron-Bost and André Schiper. The heard-of model: computing in distributed systems with benign faults. Distributed Computing, 22(1):49-71, 2009.
Andrei Damian, Cezara Drăgoi, Alexandru Militaru, and Josef Widder. Communication-closed asynchronous protocols. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV'19), volume 11562 of Lecture Notes in Computer Science, pages 344-363. Springer, 2019.
Nicolaas G. de Bruijn. A combinatorial problem. Indagationes Mathematicae, 49:758-764, 1946.
Cezara Drăgoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. A Logic-Based Framework for Verifying Consensus Algorithms. In Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'14), volume 8318 of Lecture Notes in Computer Science, pages 161-181, 2014.
Tzilla Elrad and Nissim Francez. Decomposition of distributed programs into communication-closed layers. Science of Computer Programming, 2(3):155-173, 1982.
Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science (STACS'14), volume 25 of LIPIcs, pages 1-10. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014.
Igor Konnov, Marijana Lazić, Helmut Veith, and Josef Widder. A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'17), pages 719-734, 2017.
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.
Jure Kukovec, Igor Konnov, and Josef Widder. Reachability in parameterized systems: All flavors of threshold automata. In Proceedings of the 29th International Conference on Concurrency Theory (CONCUR'18), volume 118 of LIPIcs, pages 19:1-19:17, 2018.
Leslie Lamport. Checking a multithreaded algorithm with ^+CAL. In Proceedings of the 20th International Symposium on Distributed Computing (DISC'06), volume 4167 of Lecture Notes in Computer Science, pages 151-163. Springer, 2006.
Richard J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717-721, 1975.
Ognjen Maric, Christoph Sprenger, and David A. Basin. Cutoff bounds for consensus algorithms. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV'17), volume 10427 of Lecture Notes in Computer Science, pages 217-237, 2017.
Kenneth L. McMillan. Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'01), volume 2144, pages 179-195. Springer, 2001.
Dominique Méry. Verification by Construction of Distributed Algorithms. In Proceedings of the 16th International Colloquium on Theoretical Aspects of Computing (ICTAC'19), volume 11884 of Lecture Notes in Computer Science, pages 22-38. Springer, 2019.
Arnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru, and Sébastien Tixeuil. Parameterized verification of algorithms for oblivious robots on a ring. In Proceedings of the 17th International Conference on Formal Methods in Computer Aided Design (FMCAD'17), pages 212-219. IEEE, 2017.
Ocan Sankur and Jean-Pierre Talpin. An abstraction technique for parameterized model checking of leader election protocols: Application to FTSP. In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), volume 10205 of Lecture Notes in Computer Science, pages 23-40, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_2.
https://doi.org/10.1007/978-3-662-54577-5_2
Ilina Stoilkovska, Igor Konnov, Josef Widder, and Florian Zuleger. Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), volume 11428 of Lecture Notes in Computer Science, pages 357-374, 2019.
Nathalie Bertrand, Bastien Thomas, and Josef Widder
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode