×

Verification of asynchronous programs with nested locks. (English) Zbl 1491.68105

Lokam, Satya (ed.) et al., 37th IARCS annual conference on foundations of software technology and theoretical computer science, FSTTCS 2017, IIT Kanpur, India, December 12–14, 2017. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 93, Article 11, 14 p. (2018).
Summary: In this paper, we consider asynchronous programs consisting of multiple recursive threads running in parallel. Each of the threads is equipped with a multi-set. The threads can create tasks and post them onto the multi-sets or read a task from their own. In addition, they can synchronise through a finite set of locks. In this paper, we show that the reachability problem for such class of asynchronous programs is undecidable even under the nested locking policy. We then show that the reachability problem becomes decidable (Exp-space-complete) when the locks are not allowed to be held across tasks. Finally, we show that the problem is NP-complete when in addition to previous restrictions, threads always read tasks from the same state.
For the entire collection see [Zbl 1388.68010].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. {\it Logical Methods in Computer} {\it Science}, 7(4), 2011. doi:10.2168/LMCS-7(4:4)2011. · Zbl 1237.68056
[2] Mohamed Faouzi Atig, Ahmed Bouajjani, and Tayssir Touili. Analyzing asynchronous programs with preemption.In Ramesh Hariharan, Madhavan Mukund, and V. Vinay, editors, {\it IARCS Annual Conference on Foundations of Software Technology and Theoretical} {\it Computer Science, FSTTCS 2008, December 9-11, 2008, Bangalore, India}, volume 2 of {\it LIPIcs}, pages 37-48. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2008. doi:10. 4230/LIPIcs.FSTTCS.2008.1739. · Zbl 1248.68348
[3] 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, {\it CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005,} {\it San Francisco, CA, USA, August 23-26, 2005, Proceedings}, volume 3653 of {\it Lecture Notes} {\it in Computer Science}, pages 473-487. Springer, 2005. doi:10.1007/11539452_36. · Zbl 1134.68427
[4] Michael Emmi, Shaz Qadeer, and Zvonimir Rakamaric. Delay-bounded scheduling. In Thomas Ball and Mooly Sagiv, editors, {\it Proceedings of the 38th ACM SIGPLAN-SIGACT} {\it Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, Janu-} {\it ary 26-28, 2011}, pages 411-422. ACM, 2011. doi:10.1145/1926385.1926432. · Zbl 1284.68087
[5] Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. {\it ACM Trans. Program. Lang. Syst.}, 34(1):6:1-6:48, 2012. doi:10.1145/2160910.2160915. · Zbl 1262.68038
[6] Thomas Martin Gawlitza, Peter Lammich, Markus Müller-Olm, Helmut Seidl, and Alex ander Wenner. Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. In Ranjit Jhala and David A. Schmidt, editors, {\it Verifica-} {\it tion, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI} {\it 2011, Austin, TX, USA, January 23-25, 2011. Proceedings}, volume 6538 of {\it Lecture Notes in} {\it Computer Science}, pages 199-213. Springer, 2011. doi:10.1007/978-3-642-18275-4_15. · Zbl 1317.68031
[7] Ranjit Jhala and Rupak Majumdar. Interprocedural analysis of asynchronous programs. In Martin Hofmann and Matthias Felleisen, editors, {\it Proceedings of the 34th ACM SIGPLAN-} {\it SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France,} {\it January 17-19, 2007}, pages 339-350. ACM, 2007. doi:10.1145/1190216.1190266. · Zbl 1295.68086
[8] Vineet Kahlon, Franjo Ivancic, and Aarti Gupta. Reasoning about threads communicating via locks. In Kousha Etessami and Sriram K. Rajamani, editors, {\it Computer Aided Verifica-} {\it tion, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005,} {\it Proceedings}, volume 3576 of {\it Lecture Notes in Computer Science}, pages 505-518. Springer, 2005. doi:10.1007/11513988_49. · Zbl 1081.68623
[9] Peter Lammich and Markus Müller-Olm. Conflict analysis of programs with procedures, dy namic thread creation, and monitors. In María Alpuente and Germán Vidal, editors, {\it Static} {\it Analysis, 15th International Symposium, SAS 2008, Valencia, Spain, July 16-18, 2008.} {\it Proceedings}, volume 5079 of {\it Lecture Notes in Computer Science}, pages 205-220. Springer, 2008. doi:10.1007/978-3-540-69166-2_14. · Zbl 1149.68355
[10] Shaz Qadeer and Jakob Rehof. Context-bounded model checking of concurrent software. In Nicolas Halbwachs and Lenore D. Zuck, editors, {\it Tools and Algorithms for the Construction} {\it and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the} {\it Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh,} {\it UK, April 4-8, 2005, Proceedings}, volume 3440 of {\it Lecture Notes in Computer Science}, pages 93-107. Springer, 2005. doi:10.1007/978-3-540-31980-1_7. · Zbl 1087.68598
[11] :14
[12] G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. {\it ACM} {\it Trans. Program. Lang. Syst.}, 22(2):416-430, 2000. doi:10.1145/349214.349241.
[13] Koushik Sen and Mahesh Viswanathan.Model checking multithreaded programs with asynchronous atomic methods. In Thomas Ball and Robert B. Jones, editors, {\it Computer} {\it Aided Verification, 18} · Zbl 1188.68198
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.