License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.8
URN: urn:nbn:de:0030-drops-123308
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12330/
Go to the corresponding LIPIcs Volume Portal

Brunet, Paul ; Pym, David

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

pdf-format:
LIPIcs-FSCD-2020-8.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{brunet_et_al:LIPIcs:2020:12330,
  author =	{Paul Brunet and David Pym},
  title =	{{Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{8:1--8:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Zena M. Ariola},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12330},
  URN =		{urn:nbn:de:0030-drops-123308},
  doi =		{10.4230/LIPIcs.FSCD.2020.8},
  annote =	{Keywords: Concurrent Kleene Algebra, Pomsets, Atomicity, Semantics, Separation, Local reasoning, Bunched logic, Frame rules}
}

Keywords: Concurrent Kleene Algebra, Pomsets, Atomicity, Semantics, Separation, Local reasoning, Bunched logic, Frame rules
Collection: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Issue Date: 2020
Date of publication: 28.06.2020
Supplementary Material: A formalization of Section 2 in Coq is available on github: https://github.com/monstrencage/AtomicCKA.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI