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.