Axiomatization and characterization of BSP Algorithms

June 4, 2018

Yoann Marquer et Frédéric Gava (LACL)

Bulk-Synchronous Parallel (BSP) is a well known bridging model for HPC (High Performance Computing) algorithm design. It provides a conceptual bridge between the physical implementation of the machine and the abstraction available to a programmer, while having portable and scalable performance predictions of BSP algorithms on most HPC systems. But, formally, what are BSP algorithms, and which algorithms are not BSP?
First, we extend Gurevich’s thesis, in order to axiomatically define Algo-BSP, the set of BSP algorithms. Then, we prove that ASM-BSP, an extension of Gurevich’s Abstract State Machines (ASM), captures Algo-BSP. Finally, by using a fair bisimulation, we prove that ASM-BSP is algorithmically equivalent to While-BSP, a minimal imperative language with BSP routines.
In other words, we axiomatized BSP algorithms, and proved that many usual BSP languages (those which are extensions of While-BSP) are algorithmically complete. By contrast, we provide another example of HPC language and sketch why it may not be complete for BSP algorithms.