Type Systems for Deadlock Freedom
We have developed two formalisms, listed below,
that employ deadlock avoidance so as to guarantee deadlock
freedom for low-level languages
(such as C/Phreads or the language used internally
by an optimizing compiler) with the possibilty to use unstructured locking.
The
first paper,
presents a rich type and effect system
for a language with explicit memory management primitives.
Besides deadlock freedom, the effect system guarantees additional
properties such as race freedom and memory safety. As a result, it is
quite complicated and requires extensive annotations in the language.
No implementation is available.
The second paper
presents type and effect system for deadlock avoidance only,
which is proven type safe. The work targets low-level languages
such as C/Pthreads.
Unlike the first paper, the effects are computed using inference.
We suggest you read the second paper directly
if you are interested mainly in the deadlock avoidance aspects of our work.
As part of this work, we have also developed a
prototype for C/Pthreads that
implements the proposed formal system.
Some benchmark programs
used in the second paper are also available.
We are currently extending its analysis component to
handle bigger C/Pthreads programs.
Recently, we extended our prototype
so that it can support locks residing in dynamically allocated data structures in a
context-sensitive and field-sensitive manner, stack-allocated data
structures containing lock handles, and several optimizations that
minimize the runtime overhead of deadlock avoidance.
Prodromos Gerakios, Nikolaos Papaspyrou, Konstantinos Sagonas
A Type System for Unstructured Locking that Guarantees Deadlock Freedom without Imposing a Lock Ordering
Technical report
Prodromos Gerakios, Nikolaos Papaspyrou, Konstantinos Sagonas
A Type and Effect System for Deadlock Avoidance in Low-level Languages
Technical report
Deadlock Avoidance Tool for C Programs + Benchmark Programs
Extended Deadlock Avoidance Tool for C Programs + Benchmark Programs