LIPIcs.CONCUR.2023.24.pdf
- Filesize: 0.73 MB
- 17 pages
Document
Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints
Authors
-
Part of:
Volume:
34th International Conference on Concurrency Theory (CONCUR 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-09-07
Cite AsGet BibTex
Corto Mascle, Anca Muscholl, and Igor Walukiewicz. Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.24
https://doi.org/10.4230/LIPIcs.CONCUR.2023.24
Abstract
In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. The behavior of every process is given by a pushdown automaton. We consider infinite behaviors of such systems under strong process fairness condition. A result of a potentially infinite execution of a system is a limit configuration, that is a potentially infinite tree. The verification problem is to determine if a given system has a limit configuration satisfying a given regular property. This formulation of the problem encompasses verification of reachability as well as of many liveness properties. We show that this verification problem, while undecidable in general, is decidable for nested lock usage.
We show Exptime-completeness of the verification problem. The main source of complexity is the number of parameters in the spawn operation. If the number of parameters is bounded, our algorithm works in Ptime for properties expressed by parity automata with a fixed number of ranks.
Subject Classification
ACM Subject Classification
- Theory of computation → Distributed computing models
Keywords
- Parametric systems
- Locks
- Model-checking
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Parosh Aziz Abdulla, A. Prasad Sistla, and Muralidhar Talupur. Model checking parameterized systems. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 685-725. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_21.
- S. Akshay, Paul Gastin, Shankara Narayanan Krishna, and Sparsa Roychowdhury. Revisiting underapproximate reachability for multipushdown systems. In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I, volume 12078 of Lecture Notes in Computer Science, pages 387-404. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45190-5_21.
- Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. The complexity of bounded context switching with dynamic thread creation. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 111:1-111:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.111.
- Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. Context-bounded verification of thread pools. Proc. ACM Program. Lang., 6(POPL):1-28, 2022. URL: https://doi.org/10.1145/3498678.
- 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.
- Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In Antoni W. Mazurkiewicz and Józef Winkowski, editors, CONCUR'97: Concurrency Theory, 8th International Conference, Warsaw, volume 1243 of Lecture Notes in Computer Science, pages 135-150. Springer, 1997. URL: https://doi.org/10.1007/3-540-63141-0_10.
- Ahmed Bouajjani, Markus Müller-Olm, and Tayssir Touili. Regular symbolic analysis of dynamic networks of pushdown systems. In Martín Abadi and Luca de Alfaro, editors, CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, volume 3653 of Lecture Notes in Computer Science, pages 473-487. Springer, 2005. URL: https://doi.org/10.1007/11539452_36.
- Xvisor commit message fixing issue:. URL: https://github.com/xvisor/xvisor/commit/e5dd8291b5e3f0c552b9aacc73ef2f000ae14c09.
- Marcio Diaz and Tayssir Touili. Dealing with priorities and locks for concurrent programs. In Deepak D'Souza and K. Narayan Kumar, editors, Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings, volume 10482 of Lecture Notes in Computer Science, pages 208-224. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-68167-2_15.
- Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. J. ACM, 63(1):10:1-10:48, 2016. URL: https://doi.org/10.1145/2842603.
- Marie Fortin, Anca Muscholl, and Igor Walukiewicz. Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 155-175. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_9.
- Thomas Martin Gawlitza, Peter Lammich, Markus Müller-Olm, Helmut Seidl, and Alexander Wenner. Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. In Ranjit Jhala and David A. Schmidt, editors, Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, volume 6538 of Lecture Notes in Computer Science, pages 199-213. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-18275-4_15.
-
S. A. German and P. A. Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675-735, 1992.
- Matthew Hague. Parameterised pushdown systems with non-atomic writes. In Supratik Chakraborty and Amit Kumar, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India, volume 13 of LIPIcs, pages 457-468. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2011.457.
- Vineet Kahlon. Boundedness vs. unboundedness of lock chains: Characterizing decidability of pairwise cfl-reachability for threads communicating via locks. In 2009 24th Annual IEEE Symposium on Logic In Computer Science, pages 27-36, 2009. URL: https://doi.org/10.1109/LICS.2009.45.
- Vineet Kahlon, Franjo Ivancić, and Aarti Gupta. Reasoning about threads communicating via locks. In Proceedings of the 17th International Conference on Computer Aided Verification, CAV'05, pages 505-518, Berlin, Heidelberg, 2005. Springer-Verlag. URL: https://doi.org/10.1007/11513988_49.
- Sebastian Kenter. Lock-sensitive reachability analysis for parallel recursive programs with dynamic creation of threads and locks: a graph-based approach. PhD thesis, University of Münster, Germany, 2022. URL: https://nbn-resolving.org/urn:nbn:de:hbz:6-21089543742.
- Peter Lammich. Lock sensitive analysis of parallel programs. PhD thesis, University of Münster, 2011. URL: https://nbn-resolving.org/urn:nbn:de:hbz:6-43459441169.
- Peter Lammich, Markus Müller-Olm, Helmut Seidl, and Alexander Wenner. Contextual locking for dynamic pushdown networks. In Francesco Logozzo and Manuel Fähndrich, editors, Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, volume 7935 of Lecture Notes in Computer Science, pages 477-498. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38856-9_25.
- Peter Lammich, Markus Müller-Olm, and Alexander Wenner. Predecessor sets of dynamic pushdown networks with tree-regular constraints. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 525-539. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02658-4_39.
- Anca Muscholl, Helmut Seidl, and Igor Walukiewicz. Reachability for dynamic parametric processes. In Ahmed Bouajjani and David Monniaux, editors, Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, volume 10145 of Lecture Notes in Computer Science, pages 424-441. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-52234-0_23.
- Shaz Qadeer and Jakob Rehof. Context-bounded model checking of concurrent software. In Nicolas Halbwachs and Lenore D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3440 of Lecture Notes in Computer Science, pages 93-107. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-31980-1_7.
- Salvatore La Torre, Parthasarathy Madhusudan, and Gennaro Parlato. A robust class of context-sensitive languages. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 161-170. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.9.
- Salvatore La Torre, Margherita Napoli, and Gennaro Parlato. Reachability of scope-bounded multistack pushdown systems. Inf. Comput., 275:104588, 2020. URL: https://doi.org/10.1016/j.ic.2020.104588.
- Kazuhide Yasukata, Takeshi Tsukada, and Naoki Kobayashi. Verification of higher-order concurrent programs with dynamic resource creation. In Atsushi Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 335-353, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_18.