A Type System for Unstructured Locking that Guarantees Deadlock Freedom without Imposing a Lock Ordering
arXiv:1110.4160 · doi:10.4204/EPTCS.69.4
Abstract
Deadlocks occur in concurrent programs as a consequence of cyclic resource acquisition between threads. In this paper we present a novel type system that guarantees deadlock freedom for a language with references, unstructured locking primitives, and locks which are implicitly associated with references. The proposed type system does not impose a strict lock acquisition order and thus increases programming language expressiveness.
In Proceedings PLACES 2010, arXiv:1110.3853