We present an operational semantics for parallel lazy evaluation that accurately models the parallel behaviour the non-strict parallel functional language GpH. Parallelism is modelled synchronously, that is, single reductions are carried out separately, 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 and to the best of our knowledge this is the first semantics that models 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 low level enough 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 processors.
The framework used by the semantics is flexible in that the model can easily be adapted to express other evaluation models such as sequential call-by-need and fully-speculative evaluation, non-deterministic choice and others.
@InProceedings{icfp00,
author = {{Baker-Finch}, C. and King, D.J. and Trinder, P.W.},
title = {{An Operational Semantics for Parallel Lazy Evaluation}},
booktitle = {{International Conference on Functional Programming (ICFP'00)}},
address = {Montreal, Canada, 18--20 September},
year = {2000},
note = {To appear},
}