Derivation of Efficient and Correct Functional Bulk Synchronous Parallel Programs

Introduction

With the current generalization of parallel architectures and increasing requirement of parallel computation arises the concern of applying formal methods, which allow specifications of parallel and distributed programs to be precisely stated and the conformance of an implementation to be verified using mathematical techniques. However, the complexity of parallel programs, compared to sequential ones, makes them more error-prone and difficult to verify. This calls for a strongly structured form of parallelism, which should not only be equipped with an abstraction or model that conceals much of the complexity of parallel computation, but also provide a systematic way of developing such parallelism from specifications for practically nontrivial examples.

The Bulk Synchronous Parallel (BSP) model is a model for general-purpose, architecture-independent parallel programming. The BSP model consists of three components, namely a set of processors each with a local memory, a communication network, and a mechanism for globally synchronizing the processors. A BSP program proceeds as a series of supersteps. In each superstep, a processor may operate only on values stored in local memory. Values sent through the communication network are guaranteed to arrive at the end of a superstep. Although the BSP model is simple and concise, it remains as a challenge to systematically develop efficient and correct BSP programs that meet given specifications.

We proposed, with colleagues of the University of Tokyo and the National Institute for Informatics, the first general framework, as far as we are aware, for systematic development of certified functional BSP parallel programs. More specifically, our main technical contributions can be summarized as follows:

The Work

The goals of this internship are:

Organization

References