The Essence of Parallel Algol
Stephen Brookes · Birkhäuser Boston eBooks · 1997
We consider a parallel Algol-like language, combining the λ-calculus with shared-variable parallelism. We provide a denotational semantics for this language, simultaneously adapting the possible-worlds model of Reynolds and Oles [Rey81, 01e82] to the parallel setting and generalizing the “transition traces” model of [Bro93] to the procedural setting. This semantics supports reasoning about safety and liveness properties of parallel programs, and validates a number of natural laws of program equivalence based on non-interference properties of local variables.