Programming Research Group
Logic of global synchrony
Yifeng Chen and
January 2001, 30pp.
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.