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

TL;DR

This paper extends Concurrent Kleene Algebra with 'boxes' to model protected system parts, introduces a new logic for property specification, and develops the theoretical framework connecting these concepts for better reasoning about concurrent programs.

Contribution

It introduces pomsets with boxes for modeling protection in concurrency and develops a non-state-based logic for specifying program properties within this framework.

Findings

Pomsets with boxes effectively model protected system components.

Pomset logic characterizes runtime behavior, not just state.

Theoretical framework supports local reasoning with frame rules.

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.