An Operational Semantics for Parallel Call-by-Need

Clem Baker-Finch, David King, Jon Hall and Phil Trinder. Research Report 99/1, Faculty of Mathematics & Computing, The Open University.


We present an operational semantics for parallel call-by-need, that accurately models parallel behaviour in non-strict parallel functional languages. Parallelism is modelled synchronously, that is, single reductions are carried out simultaneously, then combined, before proceeding onto the next set of reductions. Consequently the semantics has two levels, with single-step transition rules at one level and combining rules at the other. Parallel threads are modelled by labelled bindings. A set of labelled bindings corresponds to a heap, and is used to model sharing. The semantics is set at a higher level of abstraction than an abstract machine, and is therefore more suitable for proofs. At the same time, it is low level enough to allow us to reason about parallel non-strict functional languages in terms of parallelism (i.e. resource usage), as well as runtime and work done.

A shorter version of this paper has been submitted for publication.

BibTeX, PostScript, gzipped PostScript