{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:39:40Z","timestamp":1753889980334,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2013,9,17]],"date-time":"2013-09-17T00:00:00Z","timestamp":1379376000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"National Science Foundation","award":["0747041"],"award-info":[{"award-number":["0747041"]}]},{"name":"National Science Foundation","award":["1016791"],"award-info":[{"award-number":["1016791"]}]},{"name":"National Science Foundation","award":["1016989"],"award-info":[{"award-number":["1016989"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The pairwise reachability problem for a multi-threaded program asks, given\ncontrol locations in two threads, whether they can be simultaneously reached in\nan execution of the program. The problem is important for static analysis and\nis used to detect statements that are concurrently enabled. This problem is in\ngeneral undecidable even when data is abstracted and when the threads (with\nrecursion) synchronize only using a finite set of locks. Popular programming\nparadigms that limit the lock usage patterns have been identified under which\nthe pairwise reachability problem becomes decidable. In this paper, we consider\na new natural programming paradigm, called contextual locking, which ties the\nlock usage to calling patterns in each thread: we assume that locks are\nreleased in the same context that they were acquired and that every lock\nacquired by a thread in a procedure call is released before the procedure\nreturns. Our main result is that the pairwise reachability problem is\npolynomial-time decidable for this new programming paradigm as well. The\nproblem becomes undecidable if the locks are reentrant; reentrant locking is a\n\\emph{recursive locking} mechanism which allows a thread in a multi-threaded\nprogram to acquire the reentrant lock multiple times.<\/jats:p>","DOI":"10.2168\/lmcs-9(3:21)2013","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T13:44:29Z","timestamp":1385732669000},"source":"Crossref","is-referenced-by-count":1,"title":["Reachability under Contextual Locking"],"prefix":"10.46298","volume":"Volume 9, Issue 3","author":[{"given":"Remi","family":"Bonnet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rohit","family":"Chadha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2013,9,17]]},"reference":[{"key":"796:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/762\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/762\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:55:35Z","timestamp":1681242935000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/762"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,17]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-9(3:21)2013","relation":{"is-same-as":[{"id-type":"arxiv","id":"1308.2349","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1308.2349","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2013,9,17]]},"article-number":"762"}}