Lock Capabilities

The Problem: Deadlock is a common problem in shared-state concurrent programming, where there is a cycle among threads holding locks such that each thread is waiting for a lock held by another thread in the cycle. The result is a complete lack of progress for the threads involved in the deadlock. Manifestation of deadlocks is frequently non-deterministic, and potential deadlocks are often difficult to see during the design phase. This means they often persist until late in the development cycle or years after release, when fixing them can require significant reworking of synchronization disciplines. Static techniques to prevent deadlocks can find potential deadlocks as soon as they are present in code, rather than allowing them to persist longer and become more deeply ingrained in a system.

Prior Approaches: Partitioning a program's locks into a set of equivalence classes with a fixed partial ordering, and ensuring that lock acquisition obeys the ordering is sufficient to avoid deadlock. This style of prevention is often referred to as using lock levels. To the best of our knowledge, all previous static approaches use this method. The criteria are easy to reason about, and relatively straightforward to enforce statically. Unfortunately, lock levels impose some serious restrictions. The use of a partial order disallows cycles, making fine-grained locking of circular structures impossible. The partitions are also typically very broad, meaning that frequent changes to declared lock orderings can be necessary as code evolves. Two further restrictions are also common: enforcing that objects cannot move between equivalence classes, and fixing the global number of classes a priori. Fixing class membership disallows fine-grained locking for structures that require reordering. Fixing the number of classes makes it impossible to use fine-grained locking on recursive data structures of arbitrary depth. Using data structures depending on reordering, circularity or recursive structure with these approaches generally requires that whole data structures be placed under a single lock, likely sacrificing parallelism for checkability. Overall lock levels are sufficient for coarse-grained synchronization, but make it difficult or impossible to express synchronization for many fine-grained data structures.

Our Approach: We propose deadlock freedom verificaton through the use of static lock capabilities: purely static entities that are possessed by a thread for the (static) duration of a lock acquisition and that allow a thread to acquire a specific set of other locks while the capability is held. This model is more expressive than lock levels for verifying deadlock freedom of fine-grained data structures. Because only one thread at a time may possess a given capability, there is no need to fix an ordering between locks guarded by the same capability. This makes it possible to verify deadlock freedom for structures not expressible in a lock levels system, like a circular list commonly used in OS kernels for the list of running processes: any single list node may be locked in isolation, but locking multiple list nodes requires first taking a global lock, after which any number of nodes may safely be locked in any order. There is no sensible acyclic order to set on the list nodes, so in a lock level system it would not be possible to lock multiple nodes simultaneously.

Structures such as trees using fine-grained locking are also difficult to express in lock level systems, as the relative locking order of tree nodes may change over time, for example through rebalancing. For this we propose a variation on unique references that allows strong updates to part of a type, but also allows limited aliasing: partial uniqueness. Objects may have a single, non-duplicable complete reference that fully specifies the referent's type and allows strong updates to the portion of the type associating a lock with the capability required to acquire it. Partial references carry no capability association for their referent, so a strong update to the capability association on the complete reference will not invalidate partial references, and the partial references allow external aliasing of objects whose associated reference might change, allowing them to be acquired as a thread's first lock.

Publications:

• Colin S. Gordon, Michael D. Ernst, and Dan Grossman. Static Lock Capabilities for Deadlock Freedom. In Proceedings of the 7th Workshop on Types in Language Design and Implementation (TLDI'12), Philadelphia, PA, USA. January 2011.
• Technical report UW-CSE-11-10-01

Current contacts: Colin Gordon, Michael Ernst, Dan Grossman