Journal of Logical and Algebraic Methods in Programming - On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra

Sep 4, 2026

Investigates the connection between Concurrent Separation Logic (CSL), used for modular reasoning about concurrent programs, and Concurrent Kleene Algebra (CKA), which offers an axiomatic framework for concurrency models. Embeds the proof theory of a general CSL form into a CKA variation based on predicate transformers. Compares CSL models from interleaving traces with CKA-derived structures, showing CSL concurrency proof validity can occur without leveraging CKA structure while constraints still exclude some natural CSL models.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages18

Reading Time45 min

AccessFree to download

Introduction

Context on CSL

Journal of Logical and Algebraic Methods in Programming •••(••••)•••–••• Contents lists available at ScienceDirect Journal of Logical and Algebraic Methods in Programming [www.elsevier.com/locate/jlamp](www.elsevier.com/locate/jlamp) | On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra
Peter W. O’Hearn a , Rasmus L. Petersen b , Jules Villard a,∗ , Akbar Hussain c
a University College London, UK b Microsoft Research Cambridge, UK c GSM London, UK | | | --- | --- | | a r t i c l e i n f o | a b s t r a c t
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 ﬁnd, 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.
Crown Copyright © 2014 Published by Elsevier Inc. All rights reserved. | | Article history:
Received 4 June 2013
Received in revised form 2 April 2014 Accepted 1 August 2014
Available online xxxx | | | Keywords: Compositionality Concurrency Separation Logic Kleene Algebra | | 1. Introduction The topic of modular reasoning about concurrent programs has seen great progress in the past decade, with the result that intricate programs are proven much more eﬃciently (indeed, at all) see, e.g.,[34,15,44,45,31,6,7,12,20,38] for a selection. But the ﬂourishing of ideas in the area has resulted in diversity of technique, and the question arises as to whether system can be brought to the developments by ﬁnding general principles which underpin these techniques. The purpose of this paper is simple: to try to better understand the relation between two approaches which have sought such general principles: (abstract forms of) Concurrent Separation Logic (CSL) and Concurrent Kleene Algebra (CKA). We are not ready to propose a theory underpinning all of the above-mentioned developments. But we hope that the modest goal of comparing the generalist theories that we do have can pinpoint some of the strengths and weaknesses in them, and point to directions for future work. Before describing our technical results we provide some context for the paper by describing background information on CSL and CKA. * Corresponding author. [E-mail address:](E-mail address: j.villard@ucl.ac.uk)[ j.villard@ucl.ac.uk](E-mail address: j.villard@ucl.ac.uk) (J. Villard). [http://dx.doi.org/10.1016/j.jlamp.2014.08.002](http://dx.doi.org/10.1016/j.jlamp.2014.08.002) 2352-2208/Crown Copyright © 2014 Published by Elsevier Inc. All rights reserved. 2 P. W. O’Hearn et al. / Journal of Logical and Algebraic Methods in Programming •••(••••)•••–••• 1.1. Context on CSL Concurrent Separation Logic (CSL [34]) is a logic for modular reasoning about concurrent processes, in which the proof rule {p 1}c 1 {q 1} {p 2}c2 {q 2}[Concurrency] {p 1 ∗ p 2}c 1 􀀃 c2 {q 1 ∗ q 2} allows one to reason independently about concurrent processes. Given Hoare triples for c 1 and c2 , the rule allows a conclusion about their concurrent effect on separate storage, described by the separating conjunction ∗ in the precondition p 1 ∗ p 2 and postcondition q 1 ∗ q 2 . CS

FAQs

What is the main research goal of the paper?

To compare the general theories of (abstract forms of) Concurrent Separation Logic and Concurrent Kleene Algebra, clarifying their strengths, weaknesses, and relationships.

How does the paper connect CSL proof theory to Concurrent Kleene Algebra?

It embeds the proof theory of a general CSL form into a variation of CKA, with the induced CSL models constructed using predicate transformers.

Do CSL concurrency proof rules in the studied trace-interleaving models rely on CKA structure?

No. The validity of the CSL Concurrency proof rule in these models does not follow from or otherwise use the CKA structure, even though a CKA structure can still exist and yield different CSL proof-rule models.

Sep 4, 2026

Upload by Callum