This page is about a new soundness proof for concurrent separation logic (CSL)
in terms of the standard operational semantics. The new proof gives a direct
meaning to CSL judgments, explains clearly the problem with the conjunction
rule and "precise" resource invariants, and can easily be adapted to handle
extensions of CSL, such as permissions and storable locks, as well as more
advanced program logics, such as RGSep.
Viktor Vafeiadis: Concurrent separation logic and operational semantics.
In MFPS 2011.
[Slides]
Isabelle proofs
Click here for the tarball [.zip], ported to Isabelle version 2016-1 by Qin Yu and James Brotherston, or browse the pretty-printed sources online:
- Lang: The programming language and its semantics
- CSLsound: Soundness proof of concurrent separation logic
- Perm: Soundness proof of CSL + permissions
Coq proofs
The soundness proofs of CSL and RGSep have also been carried out using the Coq proof assistant. They are available in this Github repository.