CONCUR 2004 – Concurrency Theory- P2: The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency and promote its applications. Interest in this topic is continually growing, as a consequence of the importance and ubiquity of concurrent systems and their applications, and of the scientific relevance of their foundations. | 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. 1 Introduction Parallel programs involve the concurrent execution of processes which share state and are intended to cooperate interactively. It is notoriously difficult to ensure absence of runtime errors such as races in which one process changes a piece of state being used by another process and dangling pointers which may occur if two processes attempt simultaneously to deallocate the same storage. Such phenomena can cause unpredictable or irreproducible behavior. Rather than relying on assumptions about the granularity of hardware primitives it is preferable to use program design rules and proof techniques that guarantee error-freedom. The classic example is the syntax-directed logic for partial correctness properties of pointer-free parallel programs introduced by Owicki and Gries 15 building on prior work of Hoare 7 . This approach focusses on critical variables the identifiers concurrently written by one process and read or written by another. The programmer must partition the critical variables among named resources and each occurrence of a critical variable must be inside a region naming the relevant resource. Assuming that resource management is implemented by a suitable synchronization primitive such as semaphores 6 1 the design rules guarantee mutually .
