Axiomatic Proof Techniques for Parallel Programs

Abstract

This thesis presents an axiomatic method for proving certain correctness properties of parallel programs. Axioms and inference rules for partial correctness are given for two parallel programming languages: the General Parallel Language and the Restricted Parallel Language. The General language is flexible enough to represent most standard synchronizers (e.g., semaphores, events), so that programs using these synchronizers may be verified using the GPL deductive system. However, proofs for GPL programs are in general quite complex. The Restricted language reduces this complexity by requiring shared variables to be protected by critical sections, so that only one process at a time has access to them. This discipline does not significantly reduce the power of the language, and it greatly simplifies the process of program verification. Although the axioms and inference rules are primarily intended for proofs of partial correctness, there are a number of other important properties of parallel programs. We give some practical techniques which use information obtained from a partial correctness proof to derive other correctness properties, including program termination, mutual exclusion, and freedom from deadlock. A number of examples of such proofs are given. Finally, the axioms and inference rules are shown to be consistent and complete (in a special sense) with respect to an interpretive model of parallel execution. Thus the deductive system gives an accurate description of program execution and is powerful enough to yield a proof of any true partial correctness formula.