并发程序模式数据依赖问题的复杂性
Complexity of Data Dependence problems for Program Schemas with Concurrency
摘要:
判定程序中的一点是否是数据依赖于另一点的问题是程序分析的基础,并已被广泛研究。在本文中,我们认为这个问题的抽象层次的程序模式中的计算发生在Herbrand域的条款和谓词符号,它代表任意谓词功能,是允许的。给定模式S的流程图中的顶点l,(变量复制)分配和变量v,w,我们表明,这是PSPACE-难以决定是否存在一个由S定义的程序的执行,其中v持有w的初始值,至少有一个出现在执行路径上的l,如果S中任何谓词的元数有一个恒定的上界,则PSPACE中的成员资格保持不变。我们还考虑了“对偶”问题,其中v必须在l的每次出现时保持w的初始值,对此类似的结果成立。此外,前一个问题的程序与非确定性的分支(实际上,自由模式),其中分配与功能被允许被证明是多项式时间可判定的提供一个恒定的上限被放置在并发操作符的出现次数被认为是在模式。这个结果是有希望的,因为许多并发系统具有相对较少的线程(并发进程),特别是与它们具有的语句数量相比。
英文摘要:
The problem of deciding whether one point in a program is data dependent upon another is fundamental to program analysis and has been widely studied. In this paper we consider this problem at the abstraction level of program schemas in which computations occur in the Herbrand domain of terms and predicate symbols, which represent arbitrary predicate functions, are allowed. Given a vertex l in the flowchart of a schema S having only equality (variable copying) assignments and variables v,w, we show that it is PSPACE-hard to decide whether there exists an execution of a program defined by S in which v holds the initial value of w at at least one occurrence of l on the path of execution, with membership in PSPACE holding provided there is a constant upper bound on the arity of any predicate in S. We also consider the `dual' problem in which v is required to hold the initial value of w at every occurrence of l, for which the analogous results hold. Additionally, the former problem for programs with non-deterministic branching (in effect, free schemas) in which assignments with functions are allowed is proved to be polynomial-time decidable provided a constant upper bound is placed upon the number of occurrences of the concurrency operator in the schemas being considered. This result is promising since many concurrent systems have a relatively small number of threads (concurrent processes), especially when compared with the number of statements they have.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。