Oracle Semantics for Concurrent Separation Logic (Extended Version)

Abstract:

We define (with machine-checked proofs in Coq) a modular operational semantics for Concurrent C minor-a language with shared memory, spawnable threads, and first-class locks. By modular we mean that one can reason about sequential control and data-flow knowing al- most nothing about concurrency, and one can reason about concurrency knowing almost nothing about sequential control and data-flow con- structs. We present a Concurrent Separation Logic with first-class locks and threads, and prove its soundness with respect to the operational se- mantics. Using our modularity principle, we proved the sequential C.S.L.rules (those inherited from sequential Separation Logic) simply by adapt- ing Appel & Blazy's machine-checked soundness proofs. Our Concurrent C minor operational semantics is designed to connect to Leroy's optimiz- ing (sequential) C minor compiler; we propose our modular semantics as a way to adapt Leroy's compiler-correctness proofs to the concurrent set- ting. 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.