Concurrency bugs in multithreaded software: modeling and analysis using Petri nets

DOI10.1007/s10626-012-0139-xzbMath1268.93100MaRDI QIDQ2393141

Jason Stanley, Hongwei Liao, Yin Wang, Stéphane Lafortune, Terence Kelly, Hyoun Kyu Cho, Spyros A. Reveliotis, Scott A. Mahlke

Publication date: 7 August 2013

Published in: Discrete Event Dynamic Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10626-012-0139-x

zbMATH Keywords

modeling; liveness; Petri nets; reversibility; linear separability; deadlock analysis; concurrent software; discrete-event system techniques; Gadara nets; lock acquisition; shared-memory multithreaded programs

Mathematics Subject Classification ID

93C65: Discrete event control/observation systems

Related Items

A survey of siphons in Petri nets, Mixed integer programming-based liveness test for FMS with full routing flexibility, Maximally permissive deadlock avoidance for resource allocation systems with R/W-locks

Uses Software

• Gurobi
• ESC/Java
• UMDES
• RacerX
• CTrigger

Cites Work

• Integrating discrete controller synthesis into a reactive programming language compiler
• Real-time management of resource allocation systems. A discrete event systems approach.
• Modeling multithreaded applications using Petri nets
• Feedback control of Petri nets based on place invariants
• Supervisory control of concurrent systems. A Petri net structural approach.
• Introduction to Discrete Event Systems
• Deadlock avoidance in sequential resource allocation systems with multiple resource acquisitions and flexible routings
• The theory of deadlock avoidance via discrete control
• Some model theory of sheaves of modules
• Designing Compact and Maximally Permissive Deadlock Avoidance Policies for Complex Resource Allocation Systems Through Classification Theory: The Linear Case
• Unnamed Item
• Unnamed Item
• Unnamed Item