Correctness of parallel programs: The Church-Rosser approach

For many purposes, asynchronous parallel programs may be viewed as sequential but nondeterministic programs. The direct translation to nondeterministic sequential form leads to a combinatorial explosion of program size before correctness proofs can even begin. The Church-Rosser approach to correctness of asynchronous parallel programs is a flexible way to divide a correctness proof into several lemmas, no one of which requires both deep reasoning and explicit enumeration of all the control states required in the nondeterministic sequential form of the program. The approach is stated and justified abstractly, demonstrated in detail for a simple example program, and compared with other approaches to the correctness of parallel programs. The abstract formulation is independent of the model of parallelism in the example and can also be applied to nondeterminism not derived from asynchronous parallelism. We conclude with a survey of prospects for computer assisted proofs structured by the Church-Rosser approach. © 1976.