ABSTRACT
We present a technique --- lock capabilities --- for statically verifying that multithreaded programs with locks will not deadlock. Most previous work on deadlock prevention requires a strict total order on all locks held simultaneously by a thread, but such an invariant often does not hold with fine-grained locking, especially when data-structure mutations change the order locks are acquired. Lock capabilities support idioms that use fine-grained locking, such as mutable binary trees, circular lists, and arrays where each element has a different lock.
Lock capabilities do not enforce a total order and do not prevent external references to data-structure nodes. Instead, the technique reasons about static capabilities, where a thread already holding locks can attempt to acquire another lock only if its capabilities allow it. Acquiring one lock may grant a capability to acquire further locks; in data-structures where heap shape affects safe locking orders, the heap structure can induce the capability-granting relation. Deadlock-freedom follows from ensuring that the capability-granting relation is acyclic. Where necessary, we restrict aliasing with a variant of unique references to allow strong updates to the capability-granting relation, while still allowing other aliases that are used only to acquire locks while holding no locks.
We formalize our technique as a type-and-effect system, demonstrate it handles realistic challenging idioms, and use syntactic techniques (type preservation) to show it soundly prevents deadlock.
- H. Attiya, G. Ramalingam, and N. Rinetzky. Sequential Verification of Serializability. In POPL, 2010. Google ScholarDigital Library
- K. Bierhoff and J. Aldrich. Modular Typestate Checking of Aliased Objects. In OOPSLA, 2007. Google ScholarDigital Library
- R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. Permission Accounting in Separation Logic. In POPL, 2005. Google ScholarDigital Library
- G. Boudol. A Deadlock-Free Semantics for Shared Memory Concurrency. In ICTAC, 2009. Google ScholarDigital Library
- C. Boyapati, R. Lee, and M. Rinard. Ownership Types for Safe Programming: Preventing Data Races and Deadlocks. In OOPSLA, 2002. Google ScholarDigital Library
- J. Boyland. Checking Interference with Fractional Permissions. In SAS, 2003. Google ScholarDigital Library
- M. Bravenboer and Y. Smaragdakis. Strictly Declarative Specification of Sophisticated Points-to Analyses. In OOPSLA, 2009. Google ScholarDigital Library
- V. K. Chaudhri and V. Hadzilacos. Safe Locking Policies for Dynamic Databases. In PODS, 1995. Google ScholarDigital Library
- C. Flanagan and M. Abadi. Types for Safe Locking. In ESOP, 1999. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. Type-Based Race Detection for Java. In PLDI, 2000. Google ScholarDigital Library
- P. Gerakios, N. Papaspyrou, and K. Sagonas. A Type System for Unstructured Locking that Guarantees Deadlock Freedom without Imposing a Lock Ordering. In PLACES, 2010.Google Scholar
- P. Gerakios, N. Papaspyrou, and K. Sagonas. A Type and Effect System for Deadlock Avoidance in Low-level Languages. In TLDI, 2011. Google ScholarDigital Library
- C. S. Gordon, M. D. Ernst, and D. Grossman. Static Lock Capabilities for Deadlock Freedom. Technical Report UW-CSE-11--10-01, Computer Science and Engineering, University of Washington, Seattle, WA, USA, 2011.Google Scholar
- P. Haller and M. Odersky. Capabilities for Uniqueness and Borrowing. In ECOOP, 2010. Google ScholarDigital Library
- N. Kobayashi. A New Type System for Deadlock-Free Processes. In CONCUR, 2006. Google ScholarDigital Library
- K. R. Leino and P. Müller. A Basis for Verifying Multi-threaded Programs. In ESOP, 2009. Google ScholarDigital Library
- K. R. Leino, P. Müller, and J. Smans. Deadlock-free Channels and Locks. In ESOP, 2010. Google ScholarDigital Library
- F. Smith, D. Walker, and J. G. Morrisett. Alias Types. In ESOP, 2000. Google ScholarDigital Library
- D. Walker and G. Morrisett. Alias Types for Recursive Data Structures. In TIC, 2000. Google ScholarDigital Library
- D. Walker, K. Crary, and G. Morrisett. Typed Memory Management via Static Capabilities. ACM TOPLAS, 22, 2000. Google ScholarDigital Library
- Y. Wang, T. Kelly, M. Kudlur, S. Lafortune, and S. Mahlke. Gadara: Dynamic Deadlock Avoidance for Multithreaded Programs. In OSDI, 2008. Google ScholarDigital Library
- Y. Wang, S. Lafortune, T. Kelly, M. Kudlur, and S. Mahlke. The Theory of Deadlock Avoidance via Discrete Control. In POPL, 2009. Google ScholarDigital Library
Index Terms
- Static lock capabilities for deadlock freedom
Recommendations
Higher-Order Leak and Deadlock Free Locks
Reasoning about concurrent programs is challenging, especially if data is shared among threads. Program correctness can be violated by the presence of data races—whose prevention has been a topic of concern both in research and in practice. The Rust ...
Compositional deadlock detection for rendezvous communication
EMSOFT '09: Proceedings of the seventh ACM international conference on Embedded softwareConcurrent programming languages are growing in importance with the advent of multi-core systems. However, concurrent programs suffer from problems, such as data races and deadlock, absent from sequential programs. Unfortunately, traditional race and ...
Deadlock freedom through object ownership
IWACO '09: International Workshop on Aliasing, Confinement and Ownership in Object-Oriented ProgrammingActive objects are an attractive method of introducing concurrency into Java-like languages by decoupling method execution from invocation. In this paper, we show how ownership is used in the Java [14] subset language CoJava [17] to prevent deadlock ...
Comments