Dynamic Deadlock Avoidance for Multithreaded Programs via Discrete Control

We present a new approach for dynamic deadlock avoidance in concurrent programs that employ conventional mutual exclusion and synchronization primitives (e.g., multithreaded C/Pthreads programs). Beginning with control flow graphs extracted from program source code, we construct a formal model of the program and then apply Discrete Control Theory to automatically synthesize deadlock-avoidance control logic that is implemented by program instrumentation. At run time, the control logic avoids deadlocks by postponing lock acquisitions. Discrete Control Theory guarantees that the program instrumented with our synthesized control logic cannot deadlock. Our prototype for C/Pthreads scales to real software including Apache, BIND, OpenLDAP, and several benchmarks, automatically avoiding both known and injected deadlock bugs while imposing modest runtime overheads.

This work is from the PhD dissertation of Yin Wang, who just graduated and joined HP Labs in Palo Alto. It was done in collaboration with Scott Mahlke and Manjunath Kudlur of the University of Michigan and Terence Kelly of HP Labs.