ALCOMFT-TR-01-156

A. Stewart, M. Clint and J. Gabarr\'o
Algebraic rules for reasoning about BSP programs
Barcelona. Work package 4. June 2001.

Abstract: A collection of algebraic laws describing the behaviour of BSP programming structures is developed. Asynchronous communications are treated as assignments to a message relation and, as such, obey assignment laws. Supersteps are identified as compositions of independent processes followed by a barrier operation (global synchronisation) which ensures that ongoing asynchronous communications are resolved; barrier is treated as a generalised form of multiple assignment. The model has similarities to that of He et al. - for example, the construction of communication bundles. However, He's system is based on a trace model by Hoare while the approach taken here is grounded on multiple assignment and independent parallel composition. The derivation, from its sequential representation, of a parallel BSP-style version of Floyd's shortest path algorithm is used to illustrate the use of the proposed algebraic laws.

Postscript file: ALCOMFT-TR-01-156.ps.gz (96 kb).