Concurrent Separation Logic

Origin. Peter O'Hearn extended separation logic to concurrency (2004, 2007). Stephen Brookes provided semantics. Separating conjunction extends to thread separation — disjoint resources enable parallel composition. Foundation for modern concurrent program verification. Evolved into Iris, VST, and other frameworks.

Models. Ownership and concurrency. Sequential separation logic: disjoint heap ownership enables local reasoning. Concurrent separation logic: disjoint ownership enables thread-local reasoning. Threads with disjoint resources don't interfere. Shared resources require synchronization and invariants.

Formalism.

Basic concurrent rule: {P₁} C₁ {Q₁} {P₂} C₂ {Q₂} ─────────────────────────────── (disjoint) {P₁ * P₂} C₁ ∥ C₂ {Q₁ * Q₂}

If C₁ works on heap satisfying P₁ and C₂ on P₂, and they're disjoint (*), running in parallel preserves separation.

Resource invariants: Shared resources protected by locks. Resource r with invariant R:

Acquiring r: gain ownership of resource satisfying R
Releasing r: must restore R

Critical regions: {(P * Rᵣ) ∧ B} C {Q * Rᵣ} ───────────────────────────── {P} with r when B do C {Q}

The premise is about the body C alone; the conclusion is about the region. Entering hands the thread the resource invariant Rᵣ and the guard B, leaving takes Rᵣ back, and so Rᵣ never appears in the conclusion — that is what makes the invariant invisible to the rest of the program.

Ownership transfer: Threads can transfer ownership via shared data structures. Permission accounting: who owns what.

Fractional permissions: Read permission: multiple readers OK. Write permission: exclusive. π · (x ↦ v): fraction π of ownership (0 < π ≤ 1). Full ownership: 1 · (x ↦ v) = (x ↦ v).

Rely-guarantee: For fine-grained concurrency:

Rely R: what environment may do
Guarantee G: what this thread does {P, R, G} C {Q}

Modern developments:

Iris: higher-order concurrent separation logic in Coq
VST: Verified Software Toolchain
RustBelt: Rust verification

Symbols.

Symbol	Unicode	Name	Meaning
*	U+002A	Asterisk / Separating conjunction	Disjoint resources
∥	U+2225	Parallel to / Parallel composition	Two threads run interleaved
—*	—	Magic wand	Separating implication (em dash plus asterisk)
↦	U+21A6	Rightwards arrow from bar / Points-to	Heap cell ownership
π	U+03C0	Pi / Permission	Fraction of ownership, 0 < π ≤ 1
·	U+00B7	Middle dot / Scaling	π · (x ↦ v), a fraction of a cell
∧	U+2227	Conjunction	Ordinary conjunction, as in the guard (P * Rᵣ) ∧ B
□	U+25A1	Box / Persistence	Duplicable assertion
▷	U+25B7	White right-pointing triangle / Later	Step-indexed guard on recursive assertions
Rᵣ	—	Resource invariant	Invariant attached to resource r
R	—	Rely	What the environment may do
G	—	Guarantee	What this thread commits to
with r when B do C	—	Conditional critical region	Hoare's construct, CSL's unit of ownership transfer

Metatheory. O'Hearn's soundness claim was proved by Brookes (2004) using an action-trace semantics with local enabling, and the two results were recognized jointly by the 2016 Gödel Prize. Soundness is with respect to sequentially consistent interleaving semantics, and it carries a hypothesis that is not decoration: resource invariants must be precise, meaning each invariant determines a unique subheap of any state satisfying it. Reynolds' counterexample shows why — with an imprecise resource invariant such as emp ∨ (x ↦ _), the conjunction rule becomes unsound, so precision is exactly what restores {P} C {Q₁} and {P} C {Q₂} entailing {P} C {Q₁ ∧ Q₂}. The disjoint-parallelism rule delivers data-race freedom as a corollary rather than an extra proof obligation: if the two preconditions are separated, the two threads cannot touch the same cell. Fractional permissions (Boyland 2003; Bornat, Calcagno, O'Hearn, and Parkinson 2005) split a points-to assertion so that read access is shareable and write access is exactly the full fraction 1. Later frameworks — RGSep, CAP, Iris — recover ownership transfer outside syntactically scoped critical regions by moving invariants into the assertion language, with step-indexing and the ▷ modality guarding the resulting impredicativity.

Applies to. Concurrent data structure verification. Operating systems (seL4, CertiKOS). Compilers (CompCert, CakeML). Rust (ownership = separation). Lock-free algorithms. Message passing. Shared-memory concurrency.

Limitations. The soundness theorem is stated for sequential consistency; under TSO, ARM, or the C11 memory model the rules are unsound as written, and weak-memory versions must weaken the ownership reading of a points-to assertion. The precision side condition on resource invariants is required, not stylistic: drop it and the conjunction rule fails. Ownership transfer in original CSL is tied to syntactically scoped conditional critical regions, so lock-free algorithms built on compare-and-swap have no proof in the system at all — the extensions exist because the base logic cannot reach them. Every rule here is a partial-correctness rule: deadlock-freedom, starvation-freedom, and any fairness assumption are outside the assertion language, and a verified program may simply block forever. Because the assertions include arbitrary heap predicates, entailment is undecidable, and the invariants, ghost state, and permission accounting are inputs to the proof rather than outputs of an algorithm.