An SPMD parallel implementation schema for divide-and-conquer specifications is proposed and derived by formal refinement (transformation) of the specification. The specification is in the form of a mutually recursive functional definition. In a first phase, a parallel functional program schema is constructed which consists of a communication tree and a functional program that is shared by all nodes of the tree. The fact that this phase proceeds by semantics-preserving transformations in the Bird-Meertens formalism of higher-order functions guarantees the corretness of the resulting functional implementation. A second phase yields an imperative distributed SPMD implementation of this schema. The derivation process is illustrated with an example: a two-dimensional numerical intergration algorithm.
Ulrike Peiker, Martin Griebl