Parallel computers have not yet had the expected impact on mainstream computing. Parallelism adds a level of complexity to the programming task that makes it very error-prone. Moreover, a large variety of very different parallel architectures exists. Porting an implementation from one machine to another may require substantial changes.

This thesis addresses some of these problems by developing a formal basis for the design of parallel programs in form of a refinement calculus. The calculus allows the stepwise formal derivation of an abstract, low-level implementation from a trusted, high-level specification. The calculus thus helps structuring and documenting the development process. Portability is increased, because the introduction of a machine-dependent feature can be located in the refinement tree. Development efforts above this point in the tree are independent of that feature and are thus reusable. Moreover, the discovery of new, possibly more efficient solutions is facilitated. Last but not least, programs are correct by construction, which obviates the need for difficult debugging.

Our programming/specification notation supports fair parallelism, shared variable and message-passing concurrency, local variables and channels. It allows the development of reactive systems, that is, possibly non-terminating programs designed to interact persistently with their environment. Moreover, the specification of liveness properties such as termination or eventual entry is supported by our methodology.

The calculus rests on a compositional trace semenatics that treats shared-variables and message-passing concurrency uniformly. The refinement relation combines a context-sensitive notion of trace inclusion and assumption-commitment reasoning to achieve compositionality. Most refinement rules are syntax-directed in the sense that each rule corresponds to a specific language construct. The calculus straddles both concurrency paradigms. A shared-variable program can be refined into a distributed, message-passing program and vice versa. Moreover, the framework naturally extends to fine-grained levels of concurrency.

A large number of examples illustrate the use of the calculus. A complete derivation of an n-process mutual exclusion algorithm is given and more efficient versions are developed. The all-pair, shortest-paths graph problem is used to show the derivation of a distributed, message-passing program from a shared-variable parallel version.

291 pages

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

This page maintained by reports@cs.cmu.edu