Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation
Thomas Martin Gawlitza, Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner · 2011
Abstract. 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 [8]. 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. 1