On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra.

We investigate the connection between a general form of Concurrent Separation Logic (CSL), a logic for modular reasoning about concurrent programs, and Concurrent Kleene Algebra (CKA), which provides an axiomatic approach to models of concurrency. We show how the proof theory of a general form of CSL can be embedded in a variation on the notion of CKA. Our embedding, however, induces models of a particular form based on predicate transformers. We also investigate the relation between concrete models of CSL based on interleaving of traces and CKA. We find, curiously, that the validity of CSL's Concurrency proof rule in these models does not follow from or otherwise utilize CKA structure, but that a CKA structure exists nonetheless which can give a different model of the CSL proof rules.