Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
复制标题
DOI：
10.1007/978-3-642-18275-4_15
复制
发表时间：
2011-01
期刊：
影响因子：
--
通讯作者：
Thomas Gawlitza;P. Lammich;M. Müller-Olm;H. Seidl;A. Wenner
中科院分区：
文献类型：
--
作者：
Thomas Gawlitza;P. Lammich;M. Müller-Olm;H. Seidl;A. Wenner
动态下推网络（Dynamic Pushdown Networks，DPN）是一种基于递归过程和动态进程创建的并行程序模型，通过对进程生成序列的约束，可以扩展基本模型，加入已创建的进程[2]。可以通过嵌套锁定来扩展DPN [9]。存在稳定约束的正则构形集R的可达性以及无约束但有嵌套锁的可达性都是基于计算约束的集合R的可达性.在本文中，我们提出了一个前向传播算法来判断DPN的可达性。我们用执行树的集合来表示执行树的集合，并证明了所有执行树的集合是正则的，这些执行树的集合导致了从R开始的配置，这些配置允许锁敏感执行或连接敏感执行。在这里，我们依赖于基本的结果aboutmacro树换能器。作为第二个贡献，我们表明，可达性也是可判定的DPN与嵌套锁定和连接。
Dynamic Pushdown Networks (DPNs) are a model for parallel programs with (recursive) procedures and dynamic process creation.Constraintson 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 setRof configurations in presence of stable constraints as well as reachability without constraints but with nested locking are based on computing the set of predecessorspre*(R). In the present paper, we present aforward-propagating algorithm for deciding reachability for DPNs. We represent sets of executions by sets ofexecution treesand show that the set of all execution trees resulting in configurations fromRwhich either allow a lock-sensitive execution or a join-sensitive execution, isregular. Here, we rely on basic results aboutmacro tree transducers. As a second contribution, we show that reachability is decidable also for DPNs with both nested locking and joins.