UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra

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 Green open access

[img]
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 > 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
Downloads since deposit
7Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item