Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
verfasst von : Thomas Martin Gawlitza, Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner
Erschienen in: Verification, Model Checking, and Abstract Interpretation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.