We describe a formal theory of the total correctness of parallel programs, including such heretofore theoretically incomplete properties as safety from deadlock and starvation under fair-scheduling. We present a sound and complete set of proof rules for the total correctness of parallel programs expressed in nondeterministic form. The proof of soundness and completeness is novel in that we show that the weakest pre-conditions for the correctness criteria are actually fixed-points (least or greatest) of continuous functions over the complete lattice of total predicates. We have obtained proof rule schemata which can universally be applied to least or greatest fixed-points of continuous functions. Therefore, a system of proof rules is a priori sound and complete once it is shown that certain weakest pre-conditions are extremum fixed-points. The relationship between true parallelism and nondeterminism is also discussed.

We describe a formal theory of the total correctness of parallel programs, including such heretofore theoretically incomplete properties as safety from deadlock and starvation. We present a consistent and complete set of proof rules for the total correctness of parallel programs expressed in nondeterministic form. The proof of consistency and completeness is novel in that we show that the weakest preconditions for each correctness criterion are actually fixed-points (least or greatest) of continuous functions over the complete lattice of total predicates. We have obtained proof rule schemata which can universally be applied to least or greatest fixed points of continuous functions. Therefore, our proof rules are a priori consistent and complete once it is shown that certain weakest preconditions are extremum fixed-points. The relationship between true parallelism and nondeterminism is also discussed.