Concurrent Separation Logic

Origin. Peter O'Hearn extended separation logic to concurrency (2004, 2007). Stephen Brookes provided semantics. The key insight: 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} with r do C {Q * R} ───────────────────────────── {P} with r do C {Q}

Inside critical region: own resource + invariant. Outside: invariant hidden, only own P.

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
*	—	Separating conjunction	Disjoint resources
∥	U+2225	Parallel	Parallel composition
—*	—	Magic wand	Separating implication
↦	U+21A6	Points-to	Heap cell ownership
π	U+03C0	Permission	Fractional ownership
R	—	Rely	Environment assumption
G	—	Guarantee	Thread commitment
□	U+25A1	Persistent	Duplicable assertion
▷	U+25B7	Later	Step-indexed later

Metatheory. Soundness: CSL is sound for standard interleaving semantics (Brookes). Compositionality: parallel composition rule enables modular verification. Higher-order: can abstract over predicates (Iris). Step-indexing handles recursion and impredicativity. Rely-guarantee extends to fine-grained concurrency. Frame rule extends: {P}C{Q} implies {PR}C{QR} if C doesn't touch R.

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. Verification requires expertise. Invariants must be manually provided. Fine-grained concurrency needs rely-guarantee or more. Higher-order logics (Iris) are complex. Tool support improving but not push-button. Ghost state and protocol design is an art. Memory models beyond SC require extensions.