A Semantics for Concurrent Separation Logic

Concurrent separation logic is an extension of separation logic to the
shared-memory setting, allowing syntax-directed reasoning about
parallel programs that share mutable state, as proposed by Peter
O'Hearn. The logic allows correctness proofs in which "ownership" of a
piece of state such as a pointer is deemed to transfer dynamically
between processes and resources, in a manner governed by resource
invariants, with mutual exclusion for critical shared data ensured by
careful use of separating conjunction in the logical inference rules.
We present a denotational semantics based on action traces, and a more
abstract semantics based on "footstep traces", each of which can be
used to formalize the notion of ownership transfer and to prove
soundness of concurrent separation logic. As a consequence of the
soundness proof, we show that every provable program is race-free when
executed from a state satisfying the relevant pre-condition.