Formal Verification of Parallel Programs

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.

CACM July, 1976

Keller, R. M.

parallel program, correctness, verification,
assertions, deadlock, mutual exclusion, Petrinet

4.6 5.2 6.9 8.1

CA760702 JB January 4, 1978  1:20 PM

2228	4	2851
2280	4	2851
2379	4	2851
2320	4	2851
2482	4	2851
2597	4	2851
2740	4	2851
2777	4	2851
2851	4	2851
2851	4	2851
2895	4	2851
2912	4	2851
2920	4	2851
2946	4	2851
3128	4	2851
1877	5	2851
2150	5	2851
2851	5	2851
2851	5	2851
2851	5	2851