An operational semantics for parallel lazy evaluation

We present an operational semantics for parallel lazy evaluation that accur ately models the parallel behaviour of the non-strict parallel functional l anguage GPH. Parallelism is modelled synchronously, that is, single reducti ons are carried out separately then combined before proceeding to the next set of reductions. Consequently the semantics has two levels, with transiti on rules for individual threads at one level and combining rules at the oth er. Each parallel thread is modelled by a binding labelled with an indicati on of its activity status. To the best of our knowledge this is the first s emantics that models such thread states. A set of labelled bindings corresp onds to a heap and is used to model sharing. The semantics is set at a higher level of abstraction than an abstract mach ine 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 proce ssors used) as well as work and run-time with different numbers of processo rs. The framework used by the semantics is sufficiently flexible and general th at it can easily be adapted to express other evaluation models such as sequ ential call-by-need, speculative evaluation, non-deterministic choice and o thers.