Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints
Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints
复制标题
DOI：
10.1007/978-3-642-02658-4_39
复制
发表时间：
2009-06
期刊：
影响因子：
--
通讯作者：
P. Lammich;M. Müller-Olm;A. Wenner
中科院分区：
文献类型：
--
作者：
P. Lammich;M. Müller-Olm;A. Wenner
动态下推网络（DPN）是一种具有（递归）过程和进程创建的并行程序模型。本文的目标是开发通用的技术，更有表现力的可达性分析的DPNs.In本文的第一部分，我们介绍了一种新的基于树的视图上的执行。传统的交错语义模型的执行全有序序列。相反，我们通过一组部分排序的规则应用程序来建模执行，该规则应用程序仅指定每个进程的排序和由于进程创建而导致的因果关系，但并行运行的进程上的规则应用程序之间没有排序。基于树的执行允许我们计算DPN配置相对于（树）常规约束执行的常规集的前驱集。在本文的第二部分中，我们扩展了具有（良好嵌套）锁的DPN。我们将Kahlon和Gupta的捕获历史技术推广到DPN，并将本文第一部分的结果应用于计算锁敏感前导集。
Dynamic Pushdown Networks (DPNs) are a model for parallel programs with (recursive) procedures and process creation. The goal of this paper is to develop generic techniques for more expressive reachability analysis of DPNs.In the first part of the paper we introduce a new tree-based view on executions. Traditional interleaving semantics model executions by totally ordered sequences. Instead, we model an execution by a partially ordered set of rule applications, that only specifies the per-process ordering and the causality due to process creation, but no ordering between rule applications on processes that run in parallel. Tree-based executions allow us to compute predecessor sets of regular sets of DPN configurations relative to (tree-) regular constraints on executions. The corresponding problem for interleaved executions is not effective.In the second part of the paper, we extend DPNs with (well-nested) locks. We generalize Kahlon and Gupta’s technique of acquisition histories to DPNs, and apply the results of the first part of this paper to compute lock-sensitive predecessor sets.