TY - GEN
T1 - Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation
AU - Gawlitza, Thomas Martin
AU - Lammich, Peter
AU - Müller-Olm, Markus
AU - Seidl, Helmut
AU - Wenner, Alexander
N1 - Funding Information:
This work was partially funded by the DFG project OpIAT (MU 1508/1-1 and SE 551/13-1) and the ANR project ASOPT.
PY - 2011
Y1 - 2011
N2 - Dynamic Pushdown Networks (DPNs) are a model for parallel programs with (recursive) procedures and dynamic process creation. Constraints on the sequences of spawned processes allow to extend the basic model with joining of created processes [2]. Orthogonally DPNs can be extended with nested locking [9]. Reachability of a regular set R of configurations in presence of stable constraints as well as reachability without constraints but with nested locking are based on computing the set of predecessors pre *(R). In the present paper, we present a forward-propagating algorithm for deciding reachability for DPNs. We represent sets of executions by sets of execution trees and show that the set of all execution trees resulting in configurations from R which either allow a lock-sensitive execution or a join-sensitive execution, is regular. Here, we rely on basic results about macro tree transducers. As a second contribution, we show that reachability is decidable also for DPNs with both nested locking and joins.
AB - Dynamic Pushdown Networks (DPNs) are a model for parallel programs with (recursive) procedures and dynamic process creation. Constraints on the sequences of spawned processes allow to extend the basic model with joining of created processes [2]. Orthogonally DPNs can be extended with nested locking [9]. Reachability of a regular set R of configurations in presence of stable constraints as well as reachability without constraints but with nested locking are based on computing the set of predecessors pre *(R). In the present paper, we present a forward-propagating algorithm for deciding reachability for DPNs. We represent sets of executions by sets of execution trees and show that the set of all execution trees resulting in configurations from R which either allow a lock-sensitive execution or a join-sensitive execution, is regular. Here, we rely on basic results about macro tree transducers. As a second contribution, we show that reachability is decidable also for DPNs with both nested locking and joins.
UR - http://www.scopus.com/inward/record.url?scp=79251538064&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-18275-4_15
DO - 10.1007/978-3-642-18275-4_15
M3 - Conference contribution
AN - SCOPUS:79251538064
SN - 9783642182747
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 199
EP - 213
BT - Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings
T2 - 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011
Y2 - 23 January 2011 through 25 January 2011
ER -