Oracle Semantics for Concurrent Separation Logic (preliminary version) Abstract

We define in Coq with machine-checked proofs a modular operational semantics for Concurrent C minor, a language with shared memory, spawnable threads, and firstclass locks. By modular we mean that one can reason about sequential control and data-flow knowing almost nothing about concurrency, and one can reason about concurrency knowing almost nothing about sequential control and dataflow constructs. We present a generalized Concurrent Separation Logic with first-class locks and threads, and prove (in Coq) its soundness with respect to the operational semantics. Using our modularity principle, it should be straightforward to generalize Leroy’s proof of C-minor compiler correctness to the concurrent case without becoming entangled in issues of concurrency. Thus we will obtain end-to-end proofs: the properties you prove in Concurrent Separation Logic will be true of the program that actually executes on the machine. 1