Modeling Shared Variable Concurrency in Process Algebra


Process algebraic specification formalisms like CCS are based on
message passing between distributed components.
Yet, they are often used for modelling shared variable concurrency,
such as Peterson's mutual exclusion protocol.
This is done by viewing a shared memory as one of the message-passing
components.
It necessarily comes with implicit assumptions regarding progress,
justness of fairness, as well as implicit blocking when a variable is
accessed by different components.
In this talk I try to make some of these assumptions explicit.
(Note: I will focus on an idealised setting, as close as possible to
assuming sequential consistency. This talk is not about weak memory
models, trying to second-guess modern hardware.)