EAGER:Theories and Tools for Safe Concurrent Data Structures

用于推理在多处理器计算机上运行的软件的行为和正确性的现有技术假定共享存储器中的每个位置总是具有如由处理器观察到的单个唯一值。但是，在现代计算机系统中，这种假设是错误的-在不同处理器上执行的程序可能同时观察到内存中某些位置的不同值。因此，当应用于一些重要的程序类别时，现有的推理技术可能错误地断言不正确的程序实际上是正确的，从而潜在地导致运行时错误甚至安全漏洞。本研究课题的目标是开发适用于现代多处理器计算机系统的程序推理的基础理论和自动实用工具。该理论由Hoare风格的程序逻辑组成，该逻辑深入融合了x86内存模型的细节，可用于对类似C的多线程程序的部分正确性进行严格的高级证明。该逻辑受到分离逻辑的启发，并体现了x86特定的局部推理原则，该原则允许规范和证明仅限于运行时使用的资源，而不是全局系统状态。该项目还包括基于此逻辑的程序检查器，用于自动构建部分指定程序的证明。使用这些工具，该项目旨在特别针对并发数据结构：传统顺序数据结构的并发且通常易于竞争的实现，这些实现小心地省略锁和其他同步指令以最大化并发吞吐量。

Existing techniques for reasoning about the behavior and correctness of software running on multi-processor computers assume that each location in the shared memory always has a single, unique value as observed by the processors. But, on modern computer systems, this assumption is false---programs executing on different processors may simultaneously observe different values for some locations in memory. As a consequence, when applied to some important classes of programs, existing reasoning techniques may falsely assert that an incorrect program is in fact correct, thus potentially leading to runtime errors or even security breaches. The goal of this research project is to develop foundational theories and automatic, practical tools for program reasoning that are correct for such modern multi-processor computer systems.The theory consists of a Hoare-style program logic, which deeply incorporates the specifics of the x86 memory model, and which can be used to give rigorous, high-level proofs of partial correctness properties of C-like, multi-threaded programs. The logic is inspired by separation logic, and embodies a x86-specific principle of local reasoning, which allows specifications and proofs to be restricted to just those resources used at runtime, instead of the global system state. The project additionally includes program checkers based on this logic, for automatically constructing proofs of partially-specified programs. Using these tools, the project intends to target, in particular, concurrent data structures: concurrent, and typically race-prone implementations of traditional sequential data structures, which carefully omit locks and other synchronization instructions to maximize concurrent throughput.