A proof technique for parallel programs

AbstractIn this paper we present a set of axioms and rules of inference for a parallel programming language with shared variables and synchronization statements. The important difference between our approach and that of Owicki and Gries (1976) is that our semantics does not contain anything similar to their ‘interference freedom’ check, resulting in a much greater isolation of the proofs of the individual processes than is possible in their system.We illustrate our proof technique with some simple examples