Concurrent Kleene Algebra of Partial Strings

TL;DR

This paper extends the theoretical framework of Concurrent Kleene Algebra by developing a partial order model based on pomsets with fixed point operators, aiding the analysis of concurrent programs with loops and relaxed memory access.

Contribution

It introduces a partial order model of CKA using pomsets with fixed points, formalizing program refinement and enabling analysis of complex concurrent behaviors.

Findings

Constructed a partial order model of CKA based on pomsets.

Formalized program refinement using 'sik's monotonic bijective morphisms.

Provides a foundation for analyzing concurrent programs with loops and relaxed memory.

Abstract

Concurrent Kleene Algebra (CKA) is a recently proposed algebraic structure by Hoare and collaborators that unifies the laws of concurrent programming. The unifying power of CKA rests largely on the so-called exchange law that describes how concurrent and sequential composition operators can be interchanged. Based on extensive theoretical work on true concurrency in the past, this paper extends Gischer's pomset model with least fixed point operators and formalizes the program refinement relation by \'{E}sik's monotonic bijective morphisms to construct a partial order model of CKA. The existence of such a model is relevant when we want to prove and disprove properties about concurrent programs with loops. In particular, it gives a foundation for the analysis of programs that concurrently access relaxed memory as shown in subsequent work.