Idealized CSP is a programming language combining simply typed, call-by-name procedures with synchronous communicating processes. The language also generalizes Reynolds' Idealized Algol by adding typed channels and the ability to spawn parallel processes. Procedures permit the encapsulation of common communication protocols and parallel programming idioms. Local variables and local channel declarations provide a way to delimit the scope of interference between parallel agents. The combination of procedures and communicating parallelism raises significant semantic problems. We show -- perhaps surprisingly, given the fundamental differences in underlying process model -- that ideas used to model the combination of shared-variable parallelism and procedures can be adapted to the communication-based setting. This is further evidence in favor of the orthogonality of procedures and concurrency, and also shows that the shared-variable and communication-based paradigms have a lot in common, semantically. Our semantics introduces a generalization of "transition traces" and "possible worlds", incorporating an "object-oriented" treatment of channels. The semantics supports reasoning about safety and liveness properties of processes at the same time as validating natural laws of functional programming.

24 pages

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

This page maintained by [email protected]