Formal Refinement of BSP Programs with Early Cost Evaluation

The paper presents a method that allows formal refinement of BSP programs. We may consider a BSP program as a set of parameterized processes that communicate via message-passing. A parameterized process is refined into a sequence of BSP super steps each containing an ordinary sequential process and a communication process. The method uses parameterized pre- and post-conditions, and takes into account the data-distribution, even at the beginning of the construction process. The chosen data-distribution determines the way in which the parameterized specifications are built. Different types of distribution could be considered: one-dimensional, Cartesian, or set-valued distributions. From the parameterized post conditions we can evaluate the number of communications and this allows us to make a cost evaluation even at the early stages of the design. Considering different variants for data-distribution we can evaluate the different costs and then choose the best option for a certain concrete architecture. Examples are given for parallel prefix and Lagrange interpolation.