FORMAL VERIFICATION OF PARALLEL PROGRAMS
FORMAL VERIFICATION OF PARALLEL PROGRAMS
复制标题
DOI：
10.1145/360248.360251
复制
发表时间：
1976-01-01
影响因子：
22.7
通讯作者：
KELLER, RM
中科院分区：
文献类型：
--
作者：
KELLER, RM
提出了并行计算的两种形式模型：抽象概念模型和并行程序模型。前一种模型不区分控制状态和数据状态。后一种模型包括通过允许任意多个指令指针（或进程）执行程序来表示无限组控制状态的能力。提出了一种归纳原理，该原理将控制和数据状态集放在同一基础上。通过使用“位置变量”，可以观察到无需枚举所有可能的控制状态集即可表达某些正确性条件。给出的例子中使用归纳原理来证明互斥的证明。结果表明，面向断言的证明方法是归纳原理的特例。断言方法的一种特殊情况（称为并行位置断言）被证明是不完整的。然后提出“僵局”的形式化。引入了“范数”的概念，这产生了弗洛伊德证明终止技术对死锁问题的扩展。还讨论了程序模型的扩展，它允许每个进程拥有自己的局部变量并允许共享全局变量。还讨论了某些实施形式的正确性。其中包含一个附录，它将这项工作与先前关于某些逻辑公式的可满足性的工作联系起来。
Two formal models for parallel computation are presented: an abstract conceptual model and a parallel-program model. The former model does not distinguish between control and data states. The latter model includes the capability for the representation of an infinite set of control states by allowing there to be arbitrarily many instruction pointers (or processes) executing the program. An induction principle is presented which treats the control and data state sets on the same ground. Through the use of “place variables,” it is observed that certain correctness conditions can be expressed without enumeration of the set of all possible control states. Examples are presented in which the induction principle is used to demonstrate proofs of mutual exclusion. It is shown that assertions-oriented proof methods are special cases of the induction principle. A special case of the assertions method, which is called parallel place assertions, is shown to be incomplete. A formalization of “deadlock” is then presented. The concept of a “norm” is introduced, which yields an extension, to the deadlock problem, of Floyd's technique for proving termination. Also discussed is an extension of the program model which allows each process to have its own local variables and permits shared global variables. Correctness of certain forms of implementation is also discussed. An Appendix is included which relates this work to previous work on the satisfiability of certain logical formulas.