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. © Springer-Verlag 2004.
CITATION STYLE
Brookes, S. (2004). A semantics for concurrent separation logic. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3170, 16–34. https://doi.org/10.1007/978-3-540-28644-8_2
Mendeley helps you to discover research relevant for your work.