Static lock capabilities for deadlock freedom

Download: PDF, slides (PDF).

“Static lock capabilities for deadlock freedom” by Colin S. Gordon, Michael D. Ernst, and Dan Grossman. In TLDI 2012: The seventh ACM SIGPLAN Workshop on Types in Language Design and Implementation, (Philadelphia, PA, USA), Jan. 2012, pp. 67-78.
A previous version appeared as University of Washington Department of Computer Science and Engineering technical report UW-CSE-11-10-01, (Seattle, WA, USA), Oct. 2011.

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.

Download: PDF, slides (PDF).

BibTeX entry:

@inproceedings{GordonEG2012,
   author = {Colin S. Gordon and Michael D. Ernst and Dan Grossman},
   title = {Static lock capabilities for deadlock freedom},
   booktitle = {TLDI 2012: The seventh {ACM} {SIGPLAN} Workshop on Types
	in Language Design and Implementation},
   pages = {67--78},
   address = {Philadelphia, PA, USA},
   month = jan,
   year = {2012}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.