25/01/2007
Aquinas Hobor (Princeton University)
Sequential Reasoning for Concurrent Languages

Concurrency adds a great deal of power to programming languages, but is traditionally very difficult to reason about. Concurrent Separation Logic [O'Hearn '04] extends Hoare-style reasoning to concurrent programming. The original CSL had an unrealistic view of the concurrent memory model, lacked complex sequential control flow, such as multi-exit loops and function calls, and was missing many useful concurrent features, such as dynamic locks and fork. Moreover, in the original soundness proof for CSL [Brookes '04] it is difficult to reason about complex sequential control constructs, because it always requires a fully concurrent point of view. We present a preliminary new model for concurrency which allows sequential control flow to be reasoned about sequentially, even allowing proofs about sequential features in a language to be reused when concurrency is added to the language.