The Essence of Parallel Algol

We consider a parallel Algol-like language, combining procedures with shared-variable parallelism. Procedures permit encapsulation of common parallel programming idioms. Local variables provide a way to restrict interference between parallel commands. The combination of local variables, procedures, and parallelism supports a form of concurrent object-oriented programming. We provide a denotational semantics for this language, simultaneously adapting "possible worlds" to the parallel setting and generalizing "transition traces" 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. The semantics also validates familiar laws of functional programming. We also provide a relationally parametric semantics, to permit reasoning about relation-preserving properties of programs, adapting work ...

• Type: Conference
• Year: 1996
• Where: LICS
• Authors: Stephen D. Brookes
• Keywords: Automated Reasoning, LICS 1996, Local Variables, Parallel Setting, Semantics