TY - GEN
T1 - Reachability under contextual locking
AU - Chadha, Rohit
AU - Madhusudan, P.
AU - Viswanathan, Mahesh
PY - 2012
Y1 - 2012
N2 - The pairwise reachability problem for a multi-threaded program asks, given control locations in two threads, whether they can be simultaneously reached in an execution of the program. The problem is important for static analysis and is used to detect statements that are concurrently enabled. This problem is in general undecidable even when data is abstracted and when the threads (with recursion) synchronize only using a finite set of locks. Popular programming paradigms that limit the lock usage patterns have been identified under which the pairwise reachability problem becomes decidable. In this paper, we consider a new natural programming paradigm, called contextual locking, which ties the lock usage to calling patterns in each thread: we assume that locks are released in the same context that they were acquired and that every lock acquired by a thread in a procedure call is released before the procedure returns. Our main result is that the pairwise reachability problem is polynomial-time decidable for this new programming paradigm as well.
AB - The pairwise reachability problem for a multi-threaded program asks, given control locations in two threads, whether they can be simultaneously reached in an execution of the program. The problem is important for static analysis and is used to detect statements that are concurrently enabled. This problem is in general undecidable even when data is abstracted and when the threads (with recursion) synchronize only using a finite set of locks. Popular programming paradigms that limit the lock usage patterns have been identified under which the pairwise reachability problem becomes decidable. In this paper, we consider a new natural programming paradigm, called contextual locking, which ties the lock usage to calling patterns in each thread: we assume that locks are released in the same context that they were acquired and that every lock acquired by a thread in a procedure call is released before the procedure returns. Our main result is that the pairwise reachability problem is polynomial-time decidable for this new programming paradigm as well.
UR - http://www.scopus.com/inward/record.url?scp=84859308257&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84859308257&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-28756-5_30
DO - 10.1007/978-3-642-28756-5_30
M3 - Conference contribution
AN - SCOPUS:84859308257
SN - 9783642287558
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 437
EP - 450
BT - Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings
T2 - 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012
Y2 - 24 March 2012 through 1 April 2012
ER -