LIPIcs.ICALP.2022.113.pdf
- Filesize: 0.96 MB
- 20 pages
Document
Parameterized Safety Verification of Round-Based Shared-Memory Systems
Authors
Nathalie Bertrand 
,
Nicolas Markey ,
Ocan Sankur ,
-
Part of:
Volume:
49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Colloquium on Automata, Languages, and Programming (ICALP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-06-28
File
Document Identifiers
Author Details
Cite AsGet BibTex
Nathalie Bertrand, Nicolas Markey, Ocan Sankur, and Nicolas Waldburger. Parameterized Safety Verification of Round-Based Shared-Memory Systems. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 113:1-113:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ICALP.2022.113
https://doi.org/10.4230/LIPIcs.ICALP.2022.113
Abstract
We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm [James Aspnes, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For negative instances of the safety verification problem, we also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered.
Subject Classification
ACM Subject Classification
- Theory of computation → Verification by model checking
- Theory of computation → Distributed algorithms
Keywords
- Verification
- Parameterized models
- Distributed algorithms
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- C. Aiswarya, Benedikt Bollig, and Paul Gastin. An automata-theoretic approach to the verification of distributed algorithms. Information and Computation, 259(3):305-327, 2018. URL: https://doi.org/10.1016/j.ic.2017.05.006.
- Krzysztof Apt and Dexter C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22(6):307-309, May 1986. URL: https://doi.org/10.1016/0020-0190(86)90071-2.
- James Aspnes. Fast deterministic consensus in a noisy environment. Journal of Algorithms, 45(1):16-39, 2002. URL: https://doi.org/10.1016/S0196-6774(02)00220-1.
- James Aspnes. Randomized protocols for asynchronous consensus. Distributed Computing, 16(2-3):165-175, 2003. URL: https://doi.org/10.1007/s00446-002-0081-5.
- Nathalie Bertrand, Igor Konnov, Marijana Lazic, and Josef Widder. Verification of randomized consensus algorithms under round-rigid adversaries. International Journal on Software Tools Technology Transfer, 23(5):797-821, 2021. URL: https://doi.org/10.1007/s10009-020-00603-x.
- Nathalie Bertrand, Bastien Thomas, and Josef Widder. Guard automata for the verification of safety and liveness of distributed algorithms. In Proceedings of the 32nd International Conference on Concurrency Theory (CONCUR'21), volume 203 of LIPIcs, pages 15:1-15:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.15.
- 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. URL: https://doi.org/10.2200/S00658ED1V01Y201508DCT013.
- Benedikt Bollig, Fedor Ryabinin, and Arnaud Sangnier. Reachability in distributed memory automata. In Proceedings of the 29th EACSL Annual Conference on Computer Science Logic (CSL'21), volume 183 of LIPIcs, pages 13:1-13:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.13.
- Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, and Daniel Stan. Reachability in networks of register protocols under stochastic schedulers. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP'16), volume 55 of LIPIcs, pages 106:1-106:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.106.
- Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, and Rupak Majumdar. Model checking parameterized asynchronous shared-memory systems. Formal Methods Systems Design, 50(2-3):140-167, 2017. URL: https://doi.org/10.1007/s10703-016-0258-3.
- 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. URL: https://doi.org/10.4230/LIPIcs.STACS.2014.1.
- Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV'13), volume 8044 of Lecture Notes in Computer Science, pages 124-140. Springer-Verlag, July 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_8.
- Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. Journal of the ACM, 63(1):10:1-10:48, 2016. URL: https://doi.org/10.1145/2842603.
- Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675-735, July 1992. URL: https://doi.org/10.1145/146637.146681.
- Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, and Philipp Rümmer. Fair termination for parameterized probabilistic concurrent systems. 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 499-517, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_29.
- Michel Raynal and Julien Stainer. A Simple Asynchronous Shared Memory Consensus Algorithm Based on Omega and Closing Sets. In 2012 Sixth International Conference on Complex, Intelligent, and Software Intensive Systems, pages 357-364, 2012. URL: https://doi.org/10.1109/CISIS.2012.198.