Pomsets with boxes: towards Atomic CKA
Highlights
in Warsaw,
September 2019
Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a compositional framework to reason about concurrent programs. Their free model is given by series(-parallel) rational pomset languages, a standard true concurrency semantics. A key feature of CKA is provided by the weak exchange law, allowing one to partially interleave threads. For instance this enables one to consider that a specification that allows for three parallel threads can be refined in an implementation on two processors, provided all the dependencies required in the specification are satisfied.
However, when trying to use this framework to model realistic programs, this law is often too permissive. By allowing every possible interleaving, one cannot for example provide mutual exclusion guarantees. To try and address this issue while retaining the good properties of CKA (compositionality, decidability, applicability…) we modify the underlying model of pomsets to include so-called “boxes”. Boxes intuitively correspond to an “atomic{…}” construct in a parallel programming language: they isolate part of the program from interference from the rest of the concurrent environment.
In future work, we plan to develop logics — in the style of van Benthem, Hennessy, and Milner — for describing the properties of CKA models. Here we identify three key challenges: first, to establish appropriate operational/algebraic—logical equivalence theorems; second, to establish logical characterizations of the role of boxes in specifying behaviour; third, identification of local reasoning principles, such as ‘frame rules’, that will support compositional formal reasoning about properties of CKA models.
In this talk, I will present this new model of pomsets with boxes, together with semantic and axiomatic ways of reasoning about them. This is joint work with David Pym, and all the results have been verified using the proof assistant Coq.