Technical Reports
HPL-2009-202
Click here for full text:
The Theory of Deadlock Avoidance via Discrete Control
Wang, Yin; Lafortune, Stephane; Kelly, Terence; Kudlur, Manjunath; Mahlke, Scott
HP Laboratories
HPL-2009-202
Keyword(s): deadlock avoidance, discrete control theory, multithreaded software, concurrent programming
Abstract: Deadlock in multithreaded programs is an increasingly important problem as ubiquitous multicore architectures force parallelization upon an ever wider range of software. This paper presents a theoretical foundation 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 method furthermore guarantees that the control logic is maximally permissive: it postpones lock acquisitions only when necessary to prevent deadlocks, and therefore permits maximal runtime concurrency. Our prototype for C/Pthreads scales to real software including Apache, OpenLDAP, and two kinds of benchmarks, automatically avoiding both injected and naturally occurring deadlocks while imposing modest runtime overheads.
12 Pages
Additional Publication Information: Published in Principles of Programming Languages, Savannah, Georgia, Jan 2009.
External Posting Date: August 21, 2009 [Fulltext]. Approved for External Publication
Internal Posting Date: August 21, 2009 [Fulltext]