BSP-style computation: a semantic investigation

A BSP (Bulk Synchronous Parallelism) computation is characterized by the ge neration of asynchronous messages in packages during independent execution of a number of processes and their subsequent delivery at synchronization p oints. Bundling messages together represents a significant departure from t he traditional 'one communication at a time' approach. In this paper the se mantic consequences of communication packaging are explored. In particular, the BSP communication structure is identified with a general form of subst itution-predicate substitution. Predicate substitution provides a means of reasoning about the synchronized delivery of asynchronous communications wh en the immediate programming context does not explicitly refer to the varia bles that are to be updated (unlike traditional operations, such as the ass ignment e, where the names of the updated variables can be extracted from t he context). Proofs of implementations of Newton's root finding method and prefix sum are used to illustrate the practical application of the proposed approach.