research-article

The theory of deadlock avoidance via discrete control

Authors:

Scott MahlkeAuthors Info & Claims

ACM SIGPLAN Notices, Volume 44, Issue 1

Pages 252 - 263

https://doi.org/10.1145/1594834.1480913

Published: 21 January 2009 Publication History

Get Access

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.

Google Scholar

[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.

Crossref

Google Scholar

[3]

C. G. Cassandras and S. Lafortune. Introduction to Dsicrete Event Systems. Springer, second edition, 2007.

Digital Library

Google Scholar

[4]

S. Cherem, T. Chilimbi, and S. Gulwani. Inferring locks for atomic sections. In PLDI, June 2008.

Digital Library

Google Scholar

[5]

M. Emmi, J. S. Fischer, R. Jhala, and R. Majumdar. Lock allocation. In POPL, 2007.

Digital Library

Google Scholar

[6]

D. Engler and K. Ashcraft. RacerX: Effective, static detection of race conditions and deadlocks. In SOSP, 2003.

Digital Library

Google Scholar

[7]

J. L. Hellerstein, Y. Diao, S. Parekh, and D. M. Tilbury. Feedback Control of Computing Systems. Wiley, 2004.

Digital Library

Google Scholar

[8]

L. Holloway, B. Krogh, and A. Giua. A survey of Petri net methods for controlled discrete event systems. Discrete Event Dynamic Systems: Theory and Applications, 7(2):151--190, 1997.

Digital Library

Google Scholar

[9]

Intel. Intel C++ STM Compiler, Prototype Edition, January 2008.

Google Scholar

[10]

M. V. Iordache and P. J. Antsaklis. Supervisory Control of Concurrent Systems: A Petri Net Structural Approach. Birkhäuser, 2006.

Digital Library

Google Scholar

[11]

M. Isard and A. Birrell. Automatic mutual exclusion. In Proc. 11th Workshop on Hot Topics in Operating Systems, May 2007.

Digital Library

Google Scholar

[12]

K. M. Kavi, A. Moshtaghi, and D. Chen. Modeling multithreaded applications using Petri nets. International Journal of Parallel Programming, 30(5):353--371, October 2002.

Digital Library

Google Scholar

[13]

J. Larus and R. Rajwar. Transactional Memory. Morgan & Claypool, 2007.

Google Scholar

[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.

Digital Library

Google Scholar

[15]

S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In ASPLOS, 2008.

Digital Library

Google Scholar

[16]

B. McCloskey, F. Zhou, D. Gay, and E. Brewer. Autolocker: Synchronization inference for atomic sections. In POPL, 2006.

Digital Library

Google Scholar

[17]

T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541--580, April 1989.

Crossref

Google Scholar

[18]

OpenImpact. OpenIMPACT, 2008. http://www.gelato.uiuc.edu/.

Google Scholar

[19]

OpenLDAP. OpenLDAP Issue Tracking System, 2008. http://www.openldap.org/its/.

Google Scholar

[20]

C. A. Petri. Kommunikation mit Automaten. PhD thesis, Bonn: Institut für Instrumentelle Mathematik, Schriffen des IIM Nr.3, 1962.

Google Scholar

[21]

P.J. Ramadge and W.M. Wonham. Supervisory control of a class of discrete event processes. SIAM J. Control Optim., 25(1), 1987.

Digital Library

Google Scholar

[22]

W. Reisig. Petri nets. In EATCS Monographs on Theoretical Computer Science, volume 4. Springer-Verlag, Berlin, 1985.

Digital Library

Google Scholar

[23]

S. A. Reveliotis. Real-Time Management of Resource Allocation Systems: A Discrete-Event Systems Approach. Springer, New York, NY, 2005.

Google Scholar

[24]

S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A dynamic data race detector for multithreaded programs. ACM TOCS, 15(4):391--411, November 1997.

Digital Library

Google Scholar

[25]

Y. Wang, T. Kelly, and S. Lafortune. Discrete control for safe execution of IT automation workflows. In EuroSys, 2007.

Digital Library

Google Scholar

[26]

Y. Wang, T. Kelly, M. Kudlur, S. Lafortune, and S. Mahlke. Gadara: Dynamic deadlock avoidance for multithreaded programs. In OSDI, 2008a.

Digital Library

Google Scholar

[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.

Google Scholar

[28]

AdamWelc, Bratin Saha, and Ali-Reza Adl-Tabatabai. Irrevocable transactions and their applications. In SPAA, June 2008.

Google Scholar

Cited By

View all

Ferles KVan Geffen JDillig ISmaragdakis Y(2020)Symbolic Reasoning for Automatic Signal PlacementACM SIGOPS Operating Systems Review10.1145/3421473.342148254:1(64-76)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421482
Wang ZWang HLiu SSun JWang HChen J(2020)IFIX: Fixing Concurrency Bugs While They Are Introduced2020 25th International Conference on Engineering of Complex Computer Systems (ICECCS)10.1109/ICECCS51672.2020.00025(155-164)Online publication date: Oct-2020
https://doi.org/10.1109/ICECCS51672.2020.00025
Botlagunta MAgrawal SRajeshwara Rao R(2020)Dynamic Budget-Total Need Based Resource Reservation TechniqueSmart Science10.1080/23080477.2020.17782268:2(61-70)Online publication date: 17-Jun-2020
https://doi.org/10.1080/23080477.2020.1778226
Show More Cited By

Index Terms

The theory of deadlock avoidance via discrete control
1. Hardware
  1. Hardware validation
2. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Concurrent programming structures
  2. Software organization and properties
    1. Contextual software domains
      1. Operating systems
        Process management

Recommendations

Avoiding deadlock avoidance
PACT '10: Proceedings of the 19th international conference on Parallel architectures and compilation techniques

The evolution of processor architectures from single core designs with increasing clock frequencies to multi-core designs with relatively stable clock frequencies has fundamentally altered application design. Since application programmers can no longer ...
The theory of deadlock avoidance via discrete control
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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 ...
WFR-TM

Transactional Memory (TM) is a promising concurrent programming paradigm which employs transactions to achieve synchronization in accessing common data known as transactional variables. A transaction may either commit, making its updates to ...

Reviews

Reviewer: R. Clayton

Synchronizing multithreaded computations is notoriously difficult, requiring global reasoning beyond most programmers' capabilities. Automating global reasoning to discover and possibly repair faulty synchronization is one approach to relieving synchronization difficulty. This paper describes a new analysis technique that does both. The technique has four steps: first, model the program as a control-flow graph (CFG) augmented with lock information; second, model the augmented CFG as a Petri net; third, structurally analyze the Petri net to synthesize deadlock-avoiding control logic; and, four, retrofit the synthesized control logic into the program. The second and third steps are key; the Petri net model represents deadlocks as structural?that is, static?features, and control-logic synthesis exploits discrete control theory (DCT) to provide minimally invasive runtime deadlock avoidance. This technique has a number of attractive properties. A majority of the analysis is done offline, incurring minimal runtime costs and allowing full-program analysis. Deadlock prevention is based on delayed lock acquisition, which avoids introducing new deadlocks, maintains a majority of the existing concurrent behavior, and is more flexible than other synchronization mechanisms. Experiments with randomly generated dining philosophers problems, publish/subscribe server benchmarks, and the OpenLDAP and Apache production systems show the technique scales with software size, eliminates both naturally occurring and injected deadlocks, and adds modest performance overhead. Knowledge of Petri nets and DCT is necessary, although the paper is more thorough with respect to Petri nets than it is for DCT. The bibliography also reflects Petri nets' longer history, referencing useful related and follow-on work. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 44, Issue 1

POPL '09

January 2009

453 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1594834

Issue’s Table of Contents

POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2009
464 pages
ISBN:9781605583792
DOI:10.1145/1480881
General Chair:
Zhong Shao
Yale University, USA
,
Program Chair:
Benjamin C. Pierce
University of Pennsylvania, USA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 January 2009

Published in SIGPLAN Volume 44, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

87
Total Citations
View Citations
1,157
Total Downloads

Downloads (Last 12 months)33
Downloads (Last 6 weeks)2

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ferles KVan Geffen JDillig ISmaragdakis Y(2020)Symbolic Reasoning for Automatic Signal PlacementACM SIGOPS Operating Systems Review10.1145/3421473.342148254:1(64-76)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421482
Wang ZWang HLiu SSun JWang HChen J(2020)IFIX: Fixing Concurrency Bugs While They Are Introduced2020 25th International Conference on Engineering of Complex Computer Systems (ICECCS)10.1109/ICECCS51672.2020.00025(155-164)Online publication date: Oct-2020
https://doi.org/10.1109/ICECCS51672.2020.00025
Botlagunta MAgrawal SRajeshwara Rao R(2020)Dynamic Budget-Total Need Based Resource Reservation TechniqueSmart Science10.1080/23080477.2020.17782268:2(61-70)Online publication date: 17-Jun-2020
https://doi.org/10.1080/23080477.2020.1778226
Tu TLiu XSong LZhang YBahar IHerlihy MWitchel ELebeck A(2019)Understanding Real-World Concurrency Bugs in GoProceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3297858.3304069(865-878)Online publication date: 4-Apr-2019
https://dl.acm.org/doi/10.1145/3297858.3304069
Atampore FDingel JRudie K(2019)A controller synthesis framework for automated service compositionDiscrete Event Dynamic Systems10.1007/s10626-019-00282-0Online publication date: 31-Jul-2019
https://doi.org/10.1007/s10626-019-00282-0
Ferles KVan Geffen JDillig ISmaragdakis Y(2018)Symbolic reasoning for automatic signal placementACM SIGPLAN Notices10.1145/3296979.319239553:4(120-134)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192395
Lin HWang ZLiu SSun JZhang DWei GHuchard MKästner CFraser G(2018)PFix: fixing concurrency bugs based on memory access patternsProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238198(589-600)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3238147.3238198
Ferles KVan Geffen JDillig ISmaragdakis YFoster JGrossman D(2018)Symbolic reasoning for automatic signal placementProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192395(120-134)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192395
Litoiu MShaw MTamura GVillegas NMüller HGiese HRouvoy RRutten E(2018)What Can Control Theory Teach Us About Assurances in Self-Adaptive Software Systems?Software Engineering for Self-Adaptive Systems III. Assurances10.1007/978-3-319-74183-3_4(90-134)Online publication date: 18-Jan-2018
https://doi.org/10.1007/978-3-319-74183-3_4
Rutten EMarchand NSimon D(2018)Feedback Control as MAPE-K Loop in Autonomic ComputingSoftware Engineering for Self-Adaptive Systems III. Assurances10.1007/978-3-319-74183-3_12(349-373)Online publication date: 18-Jan-2018
https://doi.org/10.1007/978-3-319-74183-3_12
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Avoiding deadlock avoidance