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