The theory of deadlock avoidance via discrete control

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.

REFERENCES

• 1: Apache. Apache bug database, 2008. https://issues.apache.org/bugzilla/index.cgi.
• 2: E. R. Boer and T. Murata. Generating basis siphons and traps of Petri nets using the sign incidence matrix. IEEE Trans. on Circuits and Systems-I, 41(4):266--271, April 1994.
• 3: Christos G. Cassandras , Stephane Lafortune, Introduction to Discrete Event Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 4: Sigmund Cherem , Trishul Chilimbi , Sumit Gulwani, Inferring locks for atomic sections, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 5: Michael Emmi , Jeffrey S. Fischer , Ranjit Jhala , Rupak Majumdar, Lock allocation, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 6: Dawson Engler , Ken Ashcraft, RacerX: effective, static detection of race conditions and deadlocks, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 7: Joseph L. Hellerstein , Yixin Diao , Sujay Parekh , Dawn M. Tilbury, Feedback Control of Computing Systems, John Wiley & Sons, 2004
• 8: L. E. Holloway , B. H. Krogh , A. Giua, A Survey of Petri Net Methods for Controlled Discrete EventSystems, Discrete Event Dynamic Systems, v.7 n.2, p.151-190, April 1997 [doi>10.1023/A:1008271916548]
• 9: Intel. Intel C++ STM Compiler, Prototype Edition, January 2008.
• 10: Marian V. Iordache , Panos J. Antsaklis, Supervisory Control of Concurrent Systems: A Petri Net Structural Approach (Systems & Control: Foundations & Applications), Birkhauser, 2006
• 11: Michael Isard , Andrew Birrell, Automatic mutual exclusion, Proceedings of the 11th USENIX workshop on Hot topics in operating systems, p.1-6, May 07-09, 2007, San Diego, CA
• 12: Krishna M. Kavi , Alireza Moshtaghi , Deng-Jyi Chen, Modeling Multithreaded Applications Using Petri Nets, International Journal of Parallel Programming, v.30 n.5, p.353-371, October 2002 [doi>10.1023/A:1019917329895]
• 13: J. Larus and R. Rajwar. Transactional Memory. Morgan & Claypool, 2007.
• 14: Z. Li, M. Zhou, and N. Wu. A survey and comparison of Petri netbased deadlock prevention policies for flexible manufacturing systems. IEEE Trans. on Systems, Man, and Cybernetics-Part C, 38(2):173--188, March 2008.
• 15: Shan Lu , Soyeon Park , Eunsoo Seo , Yuanyuan Zhou, Learning from mistakes: a comprehensive study on real world concurrency bug characteristics, Proceedings of the 13th international conference on Architectural support for programming languages and operating systems, March 01-05, 2008, Seattle, WA, USA
• 16: Bill McCloskey , Feng Zhou , David Gay , Eric Brewer, Autolocker: synchronization inference for atomic sections, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.346-358, January 11-13, 2006, Charleston, South Carolina, USA
• 17: T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541--580, April 1989.
• 18: OpenImpact. OpenIMPACT, 2008. http://www.gelato.uiuc.edu/.
• 19: OpenLDAP. OpenLDAP Issue Tracking System, 2008. http://www.openldap.org/its/.
• 20: C. A. Petri. Kommunikation mit Automaten. PhD thesis, Bonn: Institut für Instrumentelle Mathematik, Schriffen des IIM Nr.3, 1962.
• 21: P. J. Ramadge , W. M. Wonham, Supervisory control of a class of discrete event processes, SIAM Journal on Control and Optimization, v.25 n.1, p.206-230, Jan. 1987 [doi>10.1137/0325013]
• 22: W. Reisig. Petri nets. In EATCS Monographs on Theoretical Computer Science, volume 4. Springer-Verlag, Berlin, 1985.
• 23: S. A. Reveliotis. Real-Time Management of Resource Allocation Systems: A Discrete-Event Systems Approach. Springer, New York, NY, 2005.
• 24: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 25: Yin Wang , Terence Kelly , Stéphane Lafortune, Discrete control for safe execution of IT automation workflows, Proceedings of the 2nd ACM SIGOPS/EuroSys European Conference on Computer Systems 2007, March 21-23, 2007, Lisbon, Portugal
• 26: Y. Wang, T. Kelly, M. Kudlur, S. Lafortune, and S. Mahlke. Gadara: Dynamic deadlock avoidance for multithreaded programs. In OSDI, 2008a.
• 27: Y. Wang, T. Kelly, M. Kudlur, S. Mahlke, and S. Lafortune. The application of supervisory control to deadlock avoidance in concurrent software. In Workshop on Discrete Event Systems, May 2008b.
• 61: AdamWelc, Bratin Saha, and Ali-Reza Adl-Tabatabai. Irrevocable transactions and their applications. In SPAA, June 2008.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
concurrent programming, discrete control theory, dynamic deadlock avoidance, multicore processors, multithreaded programming, parallel programming