Static Deadlock Freedom
Deadlock remains a problem in concurrent programs, and we want to statically verify programs as deadlock-free. While there are effective static approaches for coarse-grained locking, fine-grained locking (e.g., where each node of a data structure is protected by its own lock) remains challenging. We propose lock capabilities as an approach to statically verifying the absence of deadlock in code for fine-grained locking. A lock capability is a static capability that permits the acquisition of a specific set of locks. Acquiring a lock gives a thread additional capabilities, allowing gradual traversal of data structures using fine-grained locking. Deadlock freedom follows from enforcing a few restrictions on the relations between locks and capabilities. We have a capability type system that uses lock capabilities to prove deadlock freedom. In the past, we have also worked on statically detecting deadlocks in libraries in the absence of client code.
People
Publications
- JavaUI: Effects for Controlling UI Object Access (2013)
- Rely-Guarantee References for Refinement Types Over Aliased Mutable Data (2013)
- Static Lock Capabilities for Deadlock Freedom (2012)
- Static lock capabilities for deadlock freedom (2012)
- Static lock capabilities for deadlock freedom (2011)
- Static deadlock detection for Java libraries (2005)

cs.