2026-07-22T06:37:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:8410 2024-03-06T10:41:56Z ddc:004 open_access

Verification of Asynchronous Programs with Nested Locks Atig, Mohamed Faouzi Bouajjani, Ahmed Narayan Kumar, K. Saivasan, Prakash asynchronous programs locks concurrency multi-set pushdown systems multi-threaded programs reachability model checking verification nested lockin 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mohamed Faouzi Atig and Ahmed Bouajjani and K. Narayan Kumar and Prakash Saivasan 2018 Is Part Of LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2017.11 urn:nbn:de:0030-drops-84106 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.11 eng https://creativecommons.org/licenses/by/3.0/legalcode