The Total Correctness of Parallel Programs
- 1 May 1981
- journal article
- Published by Society for Industrial & Applied Mathematics (SIAM) in SIAM Journal on Computing
- Vol. 10 (2) , 227-246
- https://doi.org/10.1137/0210016
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 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.Keywords
This publication has 12 references indexed in Scilit:
- Computable nondeterministic functionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1978
- Soundness and Completeness of an Axiom System for Program VerificationSIAM Journal on Computing, 1978
- Arithmetical completeness in logics of programsPublished by Springer Nature ,1978
- Proving the Correctness of Multiprocess ProgramsIEEE Transactions on Software Engineering, 1977
- Formal verification of parallel programsCommunications of the ACM, 1976
- Proving monitorsCommunications of the ACM, 1976
- Strong verification of programsIEEE Transactions on Software Engineering, 1975
- MonitorsCommunications of the ACM, 1974
- A comparison of two synchronizing conceptsActa Informatica, 1972
- Synchronization of communicating processesCommunications of the ACM, 1972