Abstract

This paper proposes a parallel programming notation and a method of reasoning about programs with the following characteristics: 1. Parallel Composition The notation provides different forms of interfaces between processes; the more restrictive the interface, the simpler the proofs of process composition. A flexible interface is that of coop-erating processes with a shared address space; proofs of programs that use this interface are based on non-interference [OG76] and temporal logic [Pnu81, CM88, Lam91]. We also propose more restrictive interfaces and specifications that allow us to use the following specification-conjunction rule: the strongest specification of a parallel composition of processes is the conjunction of the strongest specifications of its components. This rule is helpful in deriving parallel programs. 2. Determinism A process that does not use certain primitives of the notation is guaranteed to be …

Date

July 24, 1992

Authors

K Mani Chandy, Carl Kesselman

Publisher

California Institute of Technology, Computer Science Department