Concurrent Kleene Algebras
Georg Struth, University of Sheffield

Since more than a decade, variants of Kleene algebras have
been used for modelling and analysing sequential programs and systems.
These algebras provide the regular operations of choice, sequential
composition and (finite and infinite) iteration; and sequential
programming constructs such that if-then-else or while-do can be
defined in this setting. The analysis of concurrent systems, however,
requires an additional operation of concurrent composition as it is
used, e.g., in process algebras such as CCS, CSP or PAP.

In this talk I will introduce Concurrent Kleene Algebras (CKAs), which
abstracts from some of the syntactic intricacies of process algebras
and introduces a very weak concurrency operator that is nevertheless
strong enough for Hoare-style reasoning about concurrent programs. I
will show that CKAs arise in a natural way from an abstract model of
independence relations over some aggregation algebra. From the
axiomatic point of view, CKAs are bi-Kleene algebras (for sequential
and concurrent composition, respectively) that interact via an
exchange law.

I will argue that this exchange law plays a fundamental role in
concurrency; similar laws have already been used in a variety of
contexts.In particular, I will discuss this law in some other models
of CKA, including formal languages with shuffle, and discuss
completeness issues.

Finally, I will show that CKAs are strong enough to allow
abstract correctness proofs of the rules of the rely/guarantee
calculus, a standard method for verifying multi-threaded programs and
programs for multi-core architectures.

(based on joint work with Tony Hoare, Bernhard Moeller and Ian Wehrman)