Remi Bonnet ; Rohit Chadha ; Mahesh Viswanathan ; P. Madhusudan - Reachability under Contextual Locking

lmcs:762 - Logical Methods in Computer Science, September 17, 2013, Volume 9, Issue 3 - https://doi.org/10.2168/LMCS-9(3:21)2013
Reachability under Contextual LockingArticle

Authors: Remi Bonnet ; Rohit Chadha ; Mahesh Viswanathan ; P. Madhusudan

    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. The problem becomes undecidable if the locks are reentrant; reentrant locking is a \emph{recursive locking} mechanism which allows a thread in a multi-threaded program to acquire the reentrant lock multiple times.


    Volume: Volume 9, Issue 3
    Published on: September 17, 2013
    Imported on: October 20, 2012
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • CAREER: The Automata Theoretic Method in Software Verification; Funder: National Science Foundation; Code: 0747041
    • CSR: Small: Verifying Simulink-Stateflow models; Funder: National Science Foundation; Code: 1016791
    • SHF: Small: Verifying Open Concurrent Real Time Systems; Funder: National Science Foundation; Code: 1016989

    1 Document citing this article

    Consultation statistics

    This page has been seen 1077 times.
    This article's PDF has been downloaded 244 times.