A semantics for 
concurrent separation logic 

Stephen Brookes 
Carnegie Mellon University 
Department of Computer Science 

Abstract. We present a denotational semantics based on action traces, 
for parallel programs which share mutable data and synchronize using 
resources and conditional critical regions. We introduce a resource-sensitive 
logic for partial correctness, adapting separation logic to the concurrent 
setting, as proposed by O’Hearn. The logic allows program proofs in 
which “ownership” of a piece of state is deemed to transfer dynamically 
between processes and resources. We prove soundness of this logic, using 
a novel “local” interpretation of traces, and we show that every provable 
program is race-free.