The Essence of Parallel ALGOL,
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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, generalizing to permit reasoning about relation-preserving properties of programs, and adapting work of OIlearn 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.
- Computer Programming and Software