A Type and Effect System for Deadlock Avoidance in Low-level Languages
- Date and Time
Thursday, January 20th, 2010 at 13:30
Polacksbacken, room 1146
The possibility to run into a deadlock is an annoying and commonly occurring hazard associated with the concurrent execution of programs. In this talk we will 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 written in C/pthreads and then links these programs with a run-time system that avoids possible deadlocks. Our benchmark results show that it is not only possible to avoid all deadlocks with a small run-time overhead, but also often achieve better throughput in highly concurrent programs by naturally reducing lock contention.