Concurrent Kleene Algebra: Completeness and Decidability
Tobias Kappé · UCL Discovery (University College London) · 2020
Concurrent Kleene Algebra (CKA) offers a set of axioms to reason about equivalence of concurrent programs, such that equivalent programs must have the same interpretation in any program semantics that respects the axioms of CKA. It builds on the well-known formalism of Kleene Algebra, which offers the same benefits for sequential programs. CKA is complete, that is, any valid equivalence can be proved from the axioms. Moreover, equivalence of programs according to CKA can be verified mechanically, i.e., equivalence is decidable. Crucial to the latter is the fact that programs can be represented as abstract machines, which admit equivalence checking. In this thesis, we investigate techniques to augment the reasoning power of CKA with additional truths particular to the program semantics at hand. Building on similar results about Kleene Algebra, we will show that for a large class of extensions, decidability and completeness can be recovered. In particular, our techniques will allow us to incorporate reasoning about interleaving, i.e., the partially sequential execution of concurrent programs, as well as control flow, such as the conditional branching and looping structures found in most programming languages. In the second half of this thesis, we will develop our own abstract machine model to represent programs modelled by Concurrent Kleene Algebra, and show that any such program can be modelled by a machine, and vice versa. We will then argue that equivalence of these automata is mechanisable, and that the correspondence between expressions and automata can be extended further to incorporate a more general form of concurrent program composition.