© 2001 by British Computer Society
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
BSP-style Computation: a Semantic Investigation
1 School of Computer Science, The Queen's University of Belfast, Belfast BT7 1NN, N. Ireland, UK Email: a.stewart@qub.ac.uk
A BSP (Bulk Synchronous Parallelism) computation is characterized by the generation of asynchronous messages in packages during independent execution of a number of processes and their subsequent delivery at synchronization points. Bundling messages together represents a significant departure from the traditional one communication at a time approach. In this paper the semantic consequences of communication packaging are explored. In particular, the BSP communication structure is identified with a general form of substitutionpredicate substitution. Predicate substitution provides a means of reasoning about the synchronized delivery of asynchronous communications when the immediate programming context does not explicitly refer to the variables that are to be updated (unlike traditional operations, such as the assignment $x := e$, where the names of the updated variables can be extracted from the context). Proofs of implementations of Newton's root finding method and prefix sum are used to illustrate the practical application of the proposed approach.
Revised 5 December, 2000.