The Theory of Deadlock Avoidance via Discrete Control

摘要

Deadlock in multithreaded programs is an increasingly importantproblem as ubiquitous multicore architectures force parallelizationupon an ever wider range of software. This paper presents a the-oretical foundation for dynamic deadlock avoidance in concurrentprograms that employ conventional mutual exclusion and synchro-nization primitives (e.g., multithreaded C/Pthreads programs). Be-ginning with control flow graphs extracted from program sourcecode, we construct a formal model of the program and then ap-ply Discrete Control Theory to automatically synthesize deadlock-avoidance control logic that is implemented by program instrumen-tation. At run time, the control logic avoids deadlocks by postpon-ing lock acquisitions. Discrete Control Theory guarantees that theprogram instrumented with our synthesized control logic cannotdeadlock. Our method furthermore guarantees that the control logicis maximally permissive: it postpones lock acquisitions only whennecessary to prevent deadlocks, and therefore permits maximal run-time concurrency. Our prototype for C/Pthreads scales to real soft-ware including Apache, OpenLDAP, and two kinds of benchmarks,automatically avoiding both injected and naturally occurring dead-locks while imposing modest runtime overheads.