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.
Related talks | ||
|
Avancées récentes sur les algèbres de Kleene concurrentes
séminaire du LACL
in Créteil,
December 2021
(in French)
.
|
More | |
|
Recent developments in concurrent Kleene algebra
JetBrains Research
in St Petersburg (remote talk),
October 2021
.
|
More | |
|
Avancées récentes sur les algèbres de Kleene concurrentes
Séminaire MAREL
in Montpellier,
April 2021
.
|
More | |
|
Avancées récentes sur les algèbres de Kleene concurrentes
Séminaire ACADIE
in Toulouse,
April 2021
.
|
More | |
|
Observations and locality in distributed processes
IRIS scientific meeting
in London,
March 2021
.
|
More | |
|
Avancées récentes sur les algèbres de Kleene concurrentes
séminaire LIRICA
in Marseille,
January 2021
(in French)
.
|
More | |
|
Avancées récentes sur les algèbres de Kleene concurrentes
Séminaire LOVE
in Paris,
January 2021
.
|
More | |
|
Recent developments in concurrent Kleene algebra
IRIS scientific meeting
in London,
December 2020
.
|
More | |
|
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
FSCD
in Paris,
July 2020
.
|
More | |
|
Recent developments in concurrent Kleene algebra
Séminaire PPS
in Paris,
June 2020
.
|
More | |
|
Pomset languages and concurrent Kleene algebra
Theory seminar - QMU
in London,
February 2018
.
|
More | |
|
Pomset languages and concurrent Kleene algebras
Séminaire automates
in Paris,
November 2017
.
|
More | |
|
On Decidability of Concurrent Kleene Algebra
CONCUR
in Berlin,
September 2017
.
|
More | |
Related papers | ||
|
Equivalence checking for weak bi-Kleene algebra
(in LMCS 2021)
with Tobias Kappé, Alexandra Silva, Bas Luttik and Fabio Zanasi. |
More | |
|
Partially Observable Concurrent Kleene Algebra
(in CONCUR 2020)
with Jana Wagemaker, Simon Docherty, Jurriaan Rot, Tobias Kappé and Alexandra Silva. |
More | |
|
Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness
(in FoSSaCS 2020)
with Tobias Kappé, Alexandra Silva, Fabio Zanasi and Jana Wagemaker. |
More | |
|
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
(in FSCD 2020)
with David Pym. |
More | |
|
On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata
(in JLAMP 2019)
with Tobias Kappé, Alexandra Silva, Bas Luttik and Fabio Zanasi. |
More | |
|
Kleene Algebra with Observations
(in CONCUR 2019)
with Tobias Kappé, Alexandra Silva, Fabio Zanasi, Jurriaan Rot and Jana Wagemaker. |
More | |
|
Concurrent Kleene Algebra: Free Model and Completeness
(in ESOP 2018)
with Tobias Kappé, Alexandra Silva and Fabio Zanasi. |
More | |
|
Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages
(in CONCUR 2017)
with Tobias Kappé, Alexandra Silva, Bas Luttik and Fabio Zanasi. |
More | |
|
On Decidability of Concurrent Kleene Algebra
(in CONCUR 2017)
with Damien Pous and Georg Struth. |
More | |