An Operational Semantics for Parallel Lazy Evaluation
Clem Baker-Finch, David King and Phil Trinder.
ICFP '00. Montreal, Canada. September, 2000.
We present an operational semantics for parallel lazy
evaluation that accurately models the parallel behaviour
of the non-strict parallel functional language GpH.
Parallelism is modelled synchronously, that is, single reductions are
carried out separately then combined before proceeding to the next
set of reductions. Consequently the semantics has two levels, with
transition rules for individual threads at one level and combining
rules at the other. Each parallel thread is modelled by a binding
labelled with an indication of its activity status. To the best of
our knowledge this is the first semantics that models such thread
states. 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 manageable for proofs about programs
rather than implementations. At the same time,
it is sufficiently low level to allow us to reason about programs in terms
of parallelism (i.e. the number of processors used) as well
as work and run-time with different numbers of
The framework used by the semantics is sufficiently flexible and
general that it can easily be adapted to express other evaluation models
such as sequential call-by-need, fully-speculative evaluation,
non-deterministic choice and others.
BibTeX, PostScript, gzipped PostScript