LIPIcs.FSTTCS.2017.11.pdf
- Filesize: 0.5 MB
- 14 pages
Document
Verification of Asynchronous Programs with Nested Locks
Authors
-
Part of:
Volume:
37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-02-12
Cite AsGet BibTex
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. Verification of Asynchronous Programs with Nested Locks. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSTTCS.2017.11
https://doi.org/10.4230/LIPIcs.FSTTCS.2017.11
Abstract
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.
Keywords
- asynchronous programs locks concurrency multi-set pushdown systems
- multi-threaded programs
- reachability
- model checking
- verification
- nested lockin
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. Logical Methods in Computer Science, 7(4), 2011. URL: http://dx.doi.org/10.2168/LMCS-7(4:4)2011.
- Mohamed Faouzi Atig, Ahmed Bouajjani, and Tayssir Touili. Analyzing asynchronous programs with preemption. In Ramesh Hariharan, Madhavan Mukund, and V. Vinay, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008, December 9-11, 2008, Bangalore, India, volume 2 of LIPIcs, pages 37-48. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2008. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2008.1739.
- 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: http://dx.doi.org/10.1007/11539452_36.
- Michael Emmi, Shaz Qadeer, and Zvonimir Rakamaric. Delay-bounded scheduling. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 411-422. ACM, 2011. URL: http://dx.doi.org/10.1145/1926385.1926432.
- Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst., 34(1):6:1-6:48, 2012. URL: http://dx.doi.org/10.1145/2160910.2160915.
- 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: http://dx.doi.org/10.1007/978-3-642-18275-4_15.
- Ranjit Jhala and Rupak Majumdar. Interprocedural analysis of asynchronous programs. In Martin Hofmann and Matthias Felleisen, editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 339-350. ACM, 2007. URL: http://dx.doi.org/10.1145/1190216.1190266.
- Vineet Kahlon, Franjo Ivancic, and Aarti Gupta. Reasoning about threads communicating via locks. In Kousha Etessami and Sriram K. Rajamani, editors, Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, volume 3576 of Lecture Notes in Computer Science, pages 505-518. Springer, 2005. URL: http://dx.doi.org/10.1007/11513988_49.
- Peter Lammich and Markus Müller-Olm. Conflict analysis of programs with procedures, dynamic thread creation, and monitors. In María Alpuente and Germán Vidal, editors, Static Analysis, 15th International Symposium, SAS 2008, Valencia, Spain, July 16-18, 2008. Proceedings, volume 5079 of Lecture Notes in Computer Science, pages 205-220. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-69166-2_14.
- 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: http://dx.doi.org/10.1007/978-3-540-31980-1_7.
- G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst., 22(2):416-430, 2000. URL: http://dx.doi.org/10.1145/349214.349241.
- Koushik Sen and Mahesh Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 300-314. Springer, 2006. URL: http://dx.doi.org/10.1007/11817963_29.