Brunet, P;
Pym, D;
(2020)
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra.
In: Ariola, ZM, (ed.)
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020).
(pp. 5:1-5:16).
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Preview |
Text
main.pdf - Published Version Download (598kB) | Preview |
Abstract
Concurrent Kleene Algebra is an elegant tool for equational reasoning about concurrent programs. An important feature of concurrent programs that is missing from CKA is the ability to restrict legal interleavings. To remedy this we extend the standard model of CKA, namely pomsets, with a new feature, called boxes, which can specify that part of the system is protected from outside interference. We study the algebraic properties of this new model. Another drawback of CKA is that the language used for expressing properties of programs is the same as that which is used to express programs themselves. This is often too restrictive for practical purposes. We provide a logic, 'pomset logic', that is an assertion language for specifying such properties, and which is interpreted on pomsets with boxes. In contrast with other approaches, this logic is not state-based, but rather characterizes the runtime behaviour of a program. We develop the basic metatheory for the relationship between pomset logic and CKA, including frame rules to support local reasoning, and illustrate this relationship with simple examples.
| Type: | Proceedings paper |
|---|---|
| Title: | Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra |
| Event: | 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) |
| Location: | Paris, France |
| Dates: | 29 June 2020 - 06 July 2020 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.4230/LIPIcs.FSCD.2020.8 |
| Publisher version: | https://doi.org/10.4230/LIPIcs.FSCD.2020.8 |
| Language: | English |
| Additional information: | This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited. |
| Keywords: | Concurrent Kleene Algebra, Pomsets, Atomicity, Semantics, Separation, Local reasoning, Bunched logic, Frame rules |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10104100 |
Archive Staff Only
 |
View Item |
