zbMATH — the first resource for mathematics

Concurrency bugs in multithreaded software: modeling and analysis using Petri nets. (English) Zbl 1268.93100
Summary: In this paper, we apply discrete-event system techniques to model and analyze the execution of concurrent software. The problem of interest is deadlock avoidance in shared-memory multithreaded programs. We employ Petri nets to systematically model multithreaded programs with lock acquisition and release operations. We define a new class of Petri nets, called Gadara nets, that arises from this modeling process. We investigate a set of important properties of Gadara nets, such as liveness, reversibility, and linear separability. We propose efficient algorithms for the verification of liveness of Gadara nets, and report experimental results on their performance. We also present modeling examples of real-world programs. The results in this paper lay the foundations for the development of effective control synthesis algorithms for Gadara nets.

93C65 Discrete event control/observation systems
93B40 Computational methods in systems theory (MSC2010)
Full Text: DOI
[1] Allen LV (2010) Verification and anomaly detection for event-based control of manufacturing systems. PhD thesis, University of Michigan
[2] Auer A, Dingel J, Rudie K (2009) Concurrency control generation for dynamic threads using discrete-event systems. In: Proc. Allerton conference on communication, control and computing
[3] Boer, ER; Murata, T, Generating basis siphons and traps of Petri nets using the sign incidence matrix, IEEE Trans Circuits Syst—I, 41, 266-271, (1994)
[4] Cano EE, Rovetto CA, Colom JM (2010) An algorithm to compute the minimal siphons in \(S\)\^{4}PR nets. In: Proc. international workshop on discrete event systems, pp 18-23
[5] Cassandras CG, Lafortune S (2008) Introduction to discrete event systems, 2nd edn. Springer, Boston · Zbl 1165.93001
[6] Chu, F; Xie, XL, Deadlock analysis of Petri nets using siphons and mathematical programming, IEEE Trans Robot Autom, 13, 793-804, (1997)
[7] Delaval G, Marchand H, Rutten E (2010) Contracts for modular discrete controller synthesis. In: Proc. ACM conference on languages, compilers and tools for embedded systems · Zbl 1273.93111
[8] Dijkstra, EW, The mathematics behind the banker’s algorithm, 308-312, (1982), New York
[9] Dragert C, Dingel J, Rudie K (2008) Generation of concurrency control code using discrete-event systems theory. In: Proc. ACM international symposium on foundations of software engineering
[10] Engler D, Ashcraft K (2003) RacerX: effective, static detection of race conditions and deadlocks. In: Proc. the 19th ACM symposium on operating systems principles · Zbl 1045.93034
[11] Ezpeleta, J; Colom, JM; Martínez, J, A Petri net based deadlock prevention policy for flexible manufacturing systems, IEEE Trans Robot Autom, 11, 173-184, (1995)
[12] Ezpeleta, J; García-Vallés, F; Colom, JM, A banker’s solution for deadlock avoidance in FMS with flexible routing and multiresource states, IEEE Trans Robot Autom, 18, 621-625, (2002)
[13] Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB, Stata R (2002) Extended static checking for Java. In: Proc. the ACM SIGPLAN 2002 conference on programming language design and implementation · Zbl 1368.68058
[14] Gamatie A, Yu H, Delaval G, Rutten E (2009) A case study on controller synthesis for data-intensive embedded system. In: Proc. international conference on embedded software and systems
[15] Giua A (1992) Petri nets as discrete event models for supervisory control. PhD thesis, Rensselaer Polytechnic Institute · Zbl 0845.93034
[16] Gurobi (2010) Gurobi optimizer. http://www.gurobi.com/
[17] Hopcroft JE, Motwani R, Ullman JD (2006) Introduction to automata theory, languages, and computation, 3rd edn. Addison Wesley
[18] Iordache MV, Antsaklis PJ (2006) Supervisory control of concurrent systems: a Petri net structural approach. Birkhäuser, Boston · Zbl 1129.93034
[19] Iordache MV, Antsaklis PJ (2009) Petri nets and programming: a survey. In: Proc. 2009 American control conference, pp 4994-4999
[20] Iordache MV, Antsaklis PJ (2010) Concurrent program synthesis based on supervisory control. In: Proc. 2010 American control conference, pp 3378-3383
[21] Jeng, M; Xie, X, Modeling and analysis of semiconductor manufacturing systems with degraded behaviors using Petri nets and siphons, IEEE Trans Robot Autom, 17, 576-588, (2001)
[22] Kavi, KM; Moshtaghi, A; Chen, D, Modeling multithreaded applications using Petri nets, Int J Parallel Program, 35, 353-371, (2002) · Zbl 1083.68578
[23] Kelly, T; Wang, Y; Lafortune, S; Mahlke, S, Eliminating concurrency bugs with control engineering, IEEE Computer, 42, 52-60, (2009)
[24] Li, Z; Zhou, M; Wu, N, A survey and comparison of Petri net-based deadlock prevention policies for flexible manufacturing systems, IEEE Trans Syst Man Cybern Part C, 38, 173-188, (2008) · Zbl 1199.15081
[25] Liao H, Lafortune S, Reveliotis S, Wang Y, Mahlke S (2010) Synthesis of maximally-permissive liveness-enforcing control policies for Gadara Petri nets. In: Proc. the 49th IEEE conference on decision and control · Zbl 1083.68578
[26] Liao H, Stanley J, Wang Y, Lafortune S, Reveliotis S, Mahlke S (2011) Deadlock-avoidance control of multithreaded software: an efficient siphon-based algorithm for Gadara Petri nets. In: Proc. the 50th IEEE conference on decision and control
[27] Liu C, Kondratyev A, Watanabe Y, Desel J, Sangiovanni-Vincentelli A (2006) Schedulability analysis of Petri nets based on structural properties. In: Proc. international conference on application of concurrency to system design · Zbl 1167.68401
[28] Murata, T, Petri nets: properties, analysis and applications, Proc IEEE, 77, 541-580, (1989)
[29] Murata, T; Shenker, B; Shatz, SM, Detection of ada static deadlocks using Petri net invariants, IEEE Trans Softw Eng, 15, 314-326, (1989)
[30] Musuvathi M, Qadeer S, Ball T, Basler G, Nainar PA, Neamtiu I (2008) Finding and reproducing Heisenbugs in concurrent programs. In: Proc. the 8th USENIX symposium on operating systems design and implementation
[31] Nazeem A, Reveliotis S, Wang Y, Lafortune S (2010) Optimal deadlock avoidance for complex resource allocation systems through classification theory. In: Proc. the 10th international workshop on discrete event systems · Zbl 1368.68058
[32] Nazeem, A; Reveliotis, S; Wang, Y; Lafortune, S, Designing compact and maximally permissive deadlock avoidance policies for complex resource allocation systems through classification theory: the linear case, IEEE Trans Autom Control, 56, 1818-1833, (2011) · Zbl 1368.68058
[33] Nir-Buchbinder Y, Tzoref R, Ur S (2008) Deadlocks: From exhibiting to healing. In: Proc. workshop on runtime verification
[34] Novark G, Berger ED, Zorn BG (2007) Exterminator: automatically correcting memory errors with high probability. In: Proc. programming language design and implementation
[35] Novark, G; Berger, ED; Zorn, BG, Exterminator: automatically correcting memory errors with high probability, Commun ACM, 51, 87-95, (2008)
[36] Park, J; Reveliotis, SA, Deadlock avoidance in sequential resource allocation systems with multiple resource acquisitions and flexible routings, IEEE Trans Autom Control, 46, 1572-1583, (2001) · Zbl 1045.93034
[37] Park, J; Reveliotis, SA, Liveness-enforcing supervision for resource allocation systems with uncontrollable behavior and forbidden states, IEEE Trans Robot Autom, 18, 234-240, (2002)
[38] Park S, Lu S, Zhou Y (2009) Ctrigger: exposing atomicity violation bugs from their hiding places. In: Proc. 14th international conference on architecture support for programming languages and operating systems
[39] Phoha, VV; Nadgar, AU; Ray, A; Phoha, S, Supervisory control of software systems, IEEE Trans Comput, 53, 1187-1199, (2004) · Zbl 1081.03035
[40] Qin F, Tucek J, Sundaresan J, Zhou Y (2005) Rx: treating bugs as allergies—a safe method to survive software failures. In: Proc. the 20th ACM symposium on operating systems principles, pp 235-248
[41] Reisig W (1985) Petri nets: an introduction. Springer, New York · Zbl 0555.68033
[42] Reveliotis SA (2005) Real-time management of resource allocation systems: a discrete-event systems approach. Springer, New York · Zbl 1069.93002
[43] Sutter, H; Larus, J, Software and the concurrency revolution, ACM Queue, 3, 54-62, (2005)
[44] Wallace C, Jensen P, Soparkar N (1996) Supervisory control of workflow scheduling. In: Proc. international workshop on advanced transaction models and architectures
[45] Wang Y (2009) Software failure avoidance using discrete control theory. PhD thesis, University of Michigan
[46] Wang Y, Kelly T, Kudlur M, Lafortune S, Mahlke SA (2008) Gadara: dynamic deadlock avoidance for multithreaded programs. In: Proc. the 8th USENIX symposium on operating systems design and implementation, pp 281-294
[47] Wang Y, Lafortune S, Kelly T, Kudlur M, Mahlke S (2009a) The theory of deadlock avoidance via discrete control. In: Proc. the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 252-263 · Zbl 1315.68073
[48] Wang Y, Liao H, Reveliotis S, Kelly T, Mahlke S, Lafortune S (2009b) Gadara nets: Modeling and analyzing lock allocation for deadlock avoidance in multithreaded software. In: Proc. the 48th IEEE conference on decision and control, pp 4971-4976
[49] Wang Y, Cho HK, Liao H, Nazeem A, Kelly TP, Lafortune S, Mahlke S, Reveliotis S (2010) Supervisory control of software execution for failure avoidance: experience from the Gadara project. In: Proc. international workshop on discrete event systems
[50] Yamalidou, K; Moody, J; Lemmon, M; Antsaklis, Pc, Feedback control of Petri nets based on place invariants, Automatica, 32, 15-28, (1996) · Zbl 0845.93034
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.