A semantics for concurrent separation logic 
Stephen Brookes 

Abstract 
We present a trace semantics for a language of parallel programs 
which share access to mutable data. We introduce a resource-sensitive 
logic for partial correctness, based on a recent proposal of O’Hearn, 
adapting separation logic to the concurrent setting. The logic allows 
proofs of parallel programs in which “ownership” of critical data, such 
as the right to access, update or deallocate a pointer, is transferred 
dynamically between concurrent processes. We prove soundness of 
the logic, using a novel “local” interpretation of traces which allows 
accurate reasoning about ownership. We show that every provable 
program is race-free.