Algorithmic Completeness of BSP Languages

The Bulk-Synchronous Parallel (BSP) bridging model is a candidate for a simple and practical definition for High Performance Computing (HPC) algorithms. These BSP algorithms have been axiomatized, then captured by the operational semantics of the BSP Abstract State Machines (ASM-BSP), an extension of the ASM model of Gurevich. In this technical report, we define a minimal imperative language While-BSP, and prove that this model of computation fairly simulates the executions of the ASM-BSP machines, and reciprocally that ASM-BSP simulates While-BSP. Therefore, While-BSP is algorithmically complete for the BSP algorithms, and so does usual programming languages like Pregel, or imperative languages using the BSPLIB library