Advertisement
Published in:
2011 | OriginalPaper | Chapter
Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
Authors : Thomas Martin Gawlitza, Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner
Published in: Verification, Model Checking, and Abstract Interpretation
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.