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