Computer Science Department
School of Computer Science, Carnegie Mellon University


The Essence of Parallel Algol

Stephen Brookes

April 1997

This is an expanded version of a paper that appeared in preliminary form in the Proceedings of the 11th IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1996.

Keywords: Programming language design, concurrent programming, semantics of programming languages, procedures, communication processes, recursion, communication

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. 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 that permits reasoning about relation-preserving properties of programs, adapting work of O'Hearn and Tennent to the parallel setting. This semantics supports standard methods of reasoning about representational independence, adapted to shared-variable programs. The clean design of the programming language and its semantics supports the orthogonality of procedures and shared-variable parallelism.

46 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by