A Software Development Methodology for BSP Model

The paper presents a method for BSP (“Bulk Synchronous Parallelism”) programs design that allows building BSP programs correct by construction. The method considers a parallel program as a number of cooperating parameterized processes with similar structures. There is no shared memory, and the communication is based on message-passing. On an abstract level, BSP is defined as a distributed memory model in which communication is separated by synchronization. So, we may reason about BSP programs as a set of parameterized processes that communicate via message-passing. The method uses parameterized pre- and post-conditions. Refinement rules of the sequential programming are used together with new rules that correspond to the new introduced program constructions. A parameterized process is refined into a sequence of BSP supersteps each containing an ordinary sequential process and a communication process. A parallel program is, thus, decomposed into layers of process instances, and the layers are considered to be communication-closed.
We can take into account the data-distribution, even at the beginning of the construction process. The possibility of counting the number of communications from postconditions, allow us to make a cost evaluation even at the early stages of the design, and so it leads us to the right decisions.