Axiomatization and characterization of BSP algorithms.

bulk-synchronous parallel (bsp ) is a 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. Two questions may come to mind. What are formally bsp algorithms? And how to ensure that the programmer can effectively program every bsp algorithm with a bsp language, especially with the right cost? gurevich proved that three convincing postulates for the sequential algorithms are equivalent to what is called abstract state machines (asms ), and thus that asms capture the sequential algorithms. Firstly, we extend these sequential postulates and asms in order to intuitively and realistically capture the bsp algorithms (and not more). Secondly, by using an operational semantics and an algorithmic simulation, we prove that Image 1 is equivalent to Image 2, a minimal imperative bsp programming language. Therefore, bsp programming languages (extending at least Image 2) are bsp algorithmically complete, involving the definition of a class model of the bsp algorithms.