Programming Research Group Research ReportRR-01-01

Logic of global synchrony

Yifeng Chen and J.W.Sanders

January 2001, 30pp.

Abstract

An intermediate-level specification notation is presented for use with BSP-style programming. It is achieved by extending pre-post semantics to reveal state at points of global synchronisation. That enables us to integrate the pre-post, finite and reactive-process styles of specification in BSP, as shown by our treatment of the dining philosophers. The language is provided with a complete set of laws and has been formulated to benefit from a simple predicative semantics.
This paper is available as a 112,057 bytes gzipped PostScript file.