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.
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 This page maintained by reports@cs.cmu.edu
School of Computer Science homepage