Keywords: Concurrency; operational semantics; memory models
Units: 12/24 units
Description: When defining the “actual” meaning of concurrent programs, one needs to handle the large number combinatorial possibilities and to cope with platform-specific behaviours, including hardware design.
For example, consider the following program.
(x := 1) ; (ra := y) || (y := 1) ; (rb := x)
After both components have finished, one would “intuitively” expect that at least one of ra and rb has value 1. We can check this by listing all six possible interleavings. However, on actual computers, it is actually possible for ra and rb to be both 0.
Not only do concurrent programs exhibit many such unintuitive behaviours, the sets of observed behaviours vary across different architectures.
The “Pipeline Semantics” is a proposed approach to explain such unintuitive behaviours, with modes built-in to model different architectures. It is an operational semantics, defined in terms of transitions on states.
Being an operation semantics, it would be useful to implement the Pipeline Semantics in Racket, a multi-paradigm programming language that comes with good supporting tools for defining the operational rules and visualising the transitions.
It is hoped that the Racket-implementation will help further investigation and development of the Pipeline Semantics.
** Prerequisites: ** Logical thinking; basic programming; the third-year course COMP3610 “Principles of Programming Languages” is ideal.