Modular verification of concurrent programs: Marrying Rely-Guarantee and Separation Logic

Reasoning about concurrent programs is difficult because of the fantastic complexity of potential interactions between concurrent processes. These problems are set to distress many more programmers with the advance of multi-core processors, where several CPU's share a common store. In the quest for tractable methods for reasoning about concurrent algorithms both rely/guarantee logic and separation logic have made great advances. They both seek to tame, or control, the complexity of concurrent interactions, but neither is the ultimate approach. Rely-guarantee copes naturally with interference, but its specifications are complex because they describe the entire state. Conversely separation logic has difficulty dealing with interference, but specifications are simpler because they describe only the relevant state, that is its footprint. We propose a new logic, which marries their strengths but not their weaknesses. Our proposal involves both fundamental theoretical work on program logic and practical work on automatic verification for this logic. Success in this project will mean a significant step towards solving the long-standing open problem of tractable reasoning about concurrency.