A Type System for Unstructured Locking that Guarantees Deadlock Freedom without Imposing a Lock Ordering

Prodromos Gerakios
(National Technical University of Athens)
Nikolaos Papaspyrou
(National Technical University of Athens)
Konstantinos Sagonas
(National Technical University of Athens)

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 Kohei Honda and Alan Mycroft: Proceedings Third Workshop on Programming Language Approaches to Concurrency and communication-cEntric Software (PLACES 2010), Paphos, Cyprus, 21st March 2010, Electronic Proceedings in Theoretical Computer Science 69, pp. 44–58.
Published: 18th October 2011.

ArXived at: https://dx.doi.org/10.4204/EPTCS.69.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org