EAGER: Automating Correctness Proofs of Transactionalized Data Structures

University Of Massachusetts Amherst, Amherst MA

Investigators

Abstract

In multi-core computing, programmers must write concurrent code to obtain performance, much harder than sequential code. Transactions are part of the solution: they reduce concurrent reasoning to sequential reasoning. But high-performance data structures require relaxed transactional memory techniques like open nesting. This places a tricky correctness burden on the programmer: identifying which operations on the data structure conflict (cannot run in simultaneous transactions), and how to undo operations to back out incomplete transactions. The proposed solution is to specify what a data structure ought to do, and to prove that the programmer's conflict and undo specifications are correct. The project will complete a proof-of-concept tool to demonstrate the feasibility of the approach. The intellectual merit includes: a language for specifying data abstractions as abstract models amenable to the proofs required; a way to describe conflicts between operations on the data type, and undos; a tool to process the descriptions and build proofs as satisfiability problems; and algorithms to prove correctness of abstract locking procotols. The project will be more successful than general program proving since it works with abstractions, not implementations, and it deals with specific properties of interest. Future work can address correctness of implementation. The broader impact consists in assisting programmers in building safe high-performance concurrent data structures for multi-core platforms. The tools and libraries produced will be widely available. Helping solve the multi-core software problem has huge implications for our economy and society.