Aquinas Hobor will present his preFPO Thursday September 20 at 10AM in room 402. The members of his committee are: Advisor Andrew Appel, Readers David Walker, Peter O'Hearn (Queen Mary College, University of London) Non-Readers: Vivek Pai, Brian Kernighan. Everyone is invited to attend his talk. His abstract follows below. Title: "Oracle Semantics for Concurrent Separation Logic" Abstract: <<< I present a model for a generalized Concurrent Separation Logic with first-class locks and threads, and prove its soundness with respect to the operational semantics of Concurrent C minor, a language with shared memory, spawnable threads, and sufficient expressive power to be the target of a C, Java, or ML compiler. The model is modular in the sense that one can reason about sequential features knowing almost nothing about concurrency, and concurrent features knowing almost nothing about sequential control flow. There are substantial, but at this point incomplete, proofs of the correctness of the system in Coq. Using the modularity principle it should be relatively straightforward to generalize Leroy's proof of C minor compiler correctness to the concurrent case without becoming deeply entangled in the 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.
Thanks, Aquinas