The operational and denotational semantics for the three concurrent imperative languages L0, L1, and L2 have previously been studied by J. W. de Bakker, Kok, and others. Both the operational and the denotational semantic models are fixed points of contractions on complete metric spaces. This differs from the common semantic approach in terms of order-theoretic domains.
The authors begin by considering the language L0, whose prominent features include parallel execution through interleaving of elementary actions, local nondeterminacy, and guarded recursive constructs. They then develop an operational semantics O 0 for L0 as the fixed point of a certain contraction and a denotational semantics D 0 as the fixed point of another contraction. O 0 and D 0 are then compared via an intermediate semantic function that is also defined as the fixed point of a contraction.
The authors follow the same approach to develop and compare operational and denotational models for L1 and L2. L1 differs from L0 both in having “communications” and in global nondeterminism. L2 is still more general in that elementary actions are no longer uninterpreted, as in L0 and L1, but are taken to be assignments, tests, and send and receive actions. Thus, the semantics of parallel execution in L1 and L2 takes into account synchronization, and in L2 it includes value passing.
The readability of this long paper is enhanced by the table of contents, the section summaries, and an appendix that reviews the mathematical concepts that are key to the authors’ methods, including Banach’s fixed point theorem. The references are helpful. The approach presented is quite general and represents a significant contribution to the difficult problem of developing satisfactory semantics for concurrent imperative languages.
