Colin S. Gordon, Michael D. Ernst, Dan Grossman
Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'12), January 2012, doi: 10.1145/2103786.2103796
Abstract
Bibtex
@inproceedings{tldi12,
author = {Colin S. Gordon and Michael D. Ernst and Dan Grossman},
title = {{Static Lock Capabilities for Deadlock Freedom}},
year = 2012,
booktitle = {{Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'12)}},
address = {{Philadelphia, PA, USA}},
month = "January",
doi = {10.1145/2103786.2103796},
abstract = {
We present a technique - lock capabilities - for statically verifying that multithreaded programs with locks will not deadlock. Most previous work is built around 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, and in data-structures where heap shape affects safe locking orders, we can use the heap structure to 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.
},
url = {http://dl.acm.org/citation.cfm?id=2103796}
}