EAGER:Theories and Tools for Safe Concurrent Data Structures

University Of Texas At Austin, Austin TX

Investigators

Abstract

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.