Paper Info
Title
Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation
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 [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.
Year
DOI
Venue
2011
10.1007/978-3-642-18275-4_15
VMCAI
Keywords
Field
DocType
reachability analysis,concurrent program,basic model,dynamic process creation,present paper,lock-sensitive execution,join-sensitive execution,regular set r,execution tree,basic result,dynamic pushdown networks,orthogonally dpns
Tree transducers,Joins,Computer science,Lock (computer science),Decidability,Theoretical computer science,Reachability,Macro,Recursion,Distributed computing
Conference
Volume
ISSN
Citations 
6538
0302-9743
16
PageRank 
References 
Authors
0.84
11
5
Name
Order
Citations
PageRank
Thomas Martin Gawlitza1886.37
Peter Lammich221225.50
Markus Müller-Olm360739.73
Helmut Seidl41468103.61
Alexander Wenner5402.81