A Semantics for Parallel Programming with BSP

The BSP model is an established practical general-purpose parallel programming model. This paper presents a semantics for the model which provides a foundation for formal development. The parallel-by-merge method is used to express parallel composition; we show that this method can be made to more accurately capture the behaviour of a BSP process if existing constraints to this approach are relaxed; this correction has consequence for many other models of shared-state concurrency. We use the model to establish some simple identities that hold in the BSP model. 1 Introduction This paper presents a predicative semantics for practical high-performance parallel computing in the BSP [15] model. BSP is an increasingly popular approach to the programming of real-world problems on practical parallel machines. The other prominent systems are PVM and MPI. These three approaches cover the vast majority of implementations of parallel applications. The BSP model is unique amongst these other model..