Consistent and complete proof rules for the total correctness of parallel programs

1 October 1978

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

No. 02725428,p. 184-192
https://doi.org/10.1109/sfcs.1978.11

Abstract

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.

Keywords

This publication has 11 references indexed in Scilit:

Nondeterminism in logics of programs
Published by Association for Computing Machinery (ACM) ,1978
Program invariants as fixed points
Published by Institute of Electrical and Electronics Engineers (IEEE) ,1977
Proving the Correctness of Multiprocess Programs
IEEE Transactions on Software Engineering, 1977
Formal verification of parallel programs
Communications of the ACM, 1976
Proving monitors
Communications of the ACM, 1976
Towards the construction of verifiable software systems
Published by Association for Computing Machinery (ACM) ,1976
Strong verification of programs
IEEE Transactions on Software Engineering, 1975
Monitors
Communications of the ACM, 1974
A comparison of two synchronizing concepts
Acta Informatica, 1972
Synchronization of communicating processes
Communications of the ACM, 1972