Logo image
Back
Static lock capabilities for deadlock freedom
Conference proceeding   Open access

Static lock capabilities for deadlock freedom

Colin S. Gordon, Michael D. Ernst and Dan Grossman
Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation, pp 67-78
28 Jan 2012
DOI: https://doi.org/10.1145/2103786.2103796
url
http://www.cs.washington.edu/homes/djg/papers/tldi12.pdfView
SubmittedOpen Access (License Unspecified),  Open

Abstract

Software and its engineering -- Software notations and tools -- General programming languages -- Language features -- Concurrent programming structures Software and its engineering -- Software organization and properties -- Software functional properties -- Correctness Theory of computation -- Logic -- Proof theory
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.

Metrics

8 Record Views
17 citations in Scopus

Details

Logo image