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

并发程序的推理是困难的，因为并发进程之间潜在的交互非常复杂。随着多核处理器的发展，这些问题将困扰更多的程序员，多个CPU共享一个公共存储。在寻求对并发算法进行推理的易处理方法的过程中，依赖/保证逻辑和分离逻辑都取得了很大的进展。它们都试图驯服或控制并发交互的复杂性，但都不是最终的方法。可靠保证自然地处理干扰，但它的规范是复杂的，因为它们描述了整个状态。相反，分离逻辑很难处理干扰，但规范更简单，因为它们只描述相关的状态，即其足迹。我们提出了一个新的逻辑，它结合了他们的优点，但不是他们的弱点。我们的建议既涉及程序逻辑的基本理论工作，也涉及这种逻辑的自动验证的实际工作。这个项目的成功将意味着朝着解决长期存在的关于并发性的易处理推理问题迈出了重要的一步。

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.