Oracle Semantics (thesis)

Abstract:

We define a Concurrent Separation Logic with first-class locks and threads for the C language, and prove its soundness in Coq with respect to a compilable operational semantics.

We define the language Concurrent C minor, an extension of the C minor language of Leroy. C minor was designed as the highest-level intermediate language in the CompCert certified ANSI C compiler, and we add to it lock, unlock, and fork statements to make Concurrent C minor, giving it a standard Pthreads style of concurrency. We define a Concurrent Separation Logic for Concurrent C minor, which extends the original Concurrent Separation Logic of O'Hearn to handle first-class locks and threads.

We then prove the soundness of the logic with respect to the operational semantics of the language. First, we define an erased concurrent operational semantics for Concurrent C minor that is a reasonable abstraction for concurrent execution on a real machine. Second, we define a new modal substructural logic which we use as the model for assertions in Concurrent Separation Logic. Third, we define an unerased concurrent operational semantics for Concurrent C minor

that keeps track of additional bookkeeping to demonstrate the programs are well-behaved. Fourth, we define an oracle semantics that is a thread-local semantics of Concurrent C minor; this allows us to separate the metatheory of sequential and concurrent computation from each other. Fifth, we give a new semantics to the Hoare tuple using our modal substructural logic that connects Concurrent Separation Logic to our oracle semantics and then connect our oracle semantics to our concurrent semantics.

Our soundness proofs are largely implemented in 60,000 lines of Coq; our modular proof design allows us to largely reuse a significant portion of the soundness proofs of the sequential subset of Concurrent Separation Logic developed by Appel and Blazy. Our ability to reuse those proofs gives us confidence that we will be able to modify the CompCert compiler proofs to handle Concurrent C minor in the future.