Concurrent Separation Logic

Concurrent separation logic (CSL) extends separation logic to reason about programs with multiple threads executing in parallel. Where classical separation logic proves that a sequential program manipulates memory safely, CSL proves that concurrent threads can share resources without race conditions — provided they respect ownership protocols that govern when memory may be read, written, or transferred between threads.

The central challenge of CSL is framing interference: when another thread might modify shared state at any moment, local reasoning about memory becomes unsound unless the logic explicitly tracks which threads own which resources. The original CSL by Peter O'Hearn restricted parallel composition to threads that accessed disjoint memory, a severe limitation that subsequent work — especially Iris — relaxed through the introduction of ghost state and shared invariants that permit controlled, logically-tracked interference.

The history of concurrent separation logic is a case study in how formal methods progress: by identifying the exact structural feature that makes a problem hard — in this case, the composition of local ownership with global sharing — and inventing mathematical machinery that makes that feature explicit rather than implicit.