View article

The possibility to run into a deadlock is an annoying and commonly occurring hazard associated with the concurrent execution of programs. In this paper we present a polymorphic type and effect system that can be used to dynamically avoid deadlocks, guided by information about the order of lock and unlock operations which is computed statically. In contrast to most other type-based approaches to deadlock freedom, our system does not insist that programs adhere to a strict lock acquisition order or use locking primitives in a block-structured way. Lifting these restrictions is primarily motivated by our desire to target low-level languages, such as C with pthreads, but it also allows our system to be directly applicable in optimizing compilers for high-level languages, such as Java.

To show the effectiveness of our approach, we have also developed a tool that uses static analysis to instrument concurrent programs …