BSP abstract state machines capture bulk synchronous parallel computations
|F. Ferrarotti, K. Schewe. BSP abstract state machines capture bulk synchronous parallel computations. Science of Computer Programming, volume 184, pages online first, DOI 10.1016/j.scico.2019.102319, 10, 2019.|
|Journal||Science of Computer Programming|
The bulk synchronous parallel (BSP) bridging model is a model for concurrent computations with alternating computation and communication phases between programs running on different processors. In a computation phase the programs proceed independently and asynchronously until a barrier is reached. In a communication phase initiated by all programs having reached the barrier only messages between the programs are exchanged until normal processing can be continued. In this article we present a behavioural theory for BSP computations comprising an axiomatisation of the BSP model, the definition of a restricted class of concurrent abstract state machines, which we call BSP abstract state machines, and the proof that BSP abstract state machines capture BSP computations as defined by the axiomatisation. We illustrate the use of BSP abstract state machines on map-reduce.