On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra

• Weak Concurrent Kleene Algebras satisfy the axioms of Concurrent Separation Logic.
• Predicate transformers form a weak CKA for which CSL is complete.
• The CKA structure of some models of CSL cannot be used to justify soundness.

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.Our results can be read as providing a completeness theorem showing a sense in which nothing is missing as far as proof power goes in (a variant on) the notion of CKA, while at the same time showing that CKAs impose constraints that rule out some natural CSL models.