DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2020.8

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

Authors: Paul Brunet and David Pym

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

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.

Cite as

Paul Brunet and David Pym. Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{brunet_et_al:LIPIcs.FSCD.2020.8,
  author =	{Brunet, Paul and Pym, David},
  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 =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.8},
  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}
}

Document

DOI: 10.4230/DagSemRep.303

Semantic Foundations of Proof-search (Dagstuhl Seminar 01141)

Authors: David Pym, Eike Ritter, and Thomas Streicher

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract

Cite as

David Pym, Eike Ritter, and Thomas Streicher. Semantic Foundations of Proof-search (Dagstuhl Seminar 01141). Dagstuhl Seminar Report 303, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2001)

Copy BibTex To Clipboard

@TechReport{pym_et_al:DagSemRep.303,
  author =	{Pym, David and Ritter, Eike and Streicher, Thomas},
  title =	{{Semantic Foundations of Proof-search (Dagstuhl Seminar 01141)}},
  pages =	{1--16},
  ISSN =	{1619-0203},
  year =	{2001},
  type = 	{Dagstuhl Seminar Report},
  number =	{303},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.303},
  URN =		{urn:nbn:de:0030-drops-151879},
  doi =		{10.4230/DagSemRep.303},
}

Search Results

Documents authored by Pym, David

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

Abstract

Cite as

Semantic Foundations of Proof-search (Dagstuhl Seminar 01141)

Abstract

Cite as

Thanks for your feedback!

Could not send message