EAGER: Automating Correctness Proofs of Transactionalized Data Structures

点击翻译按钮获取中文摘要

In multi-core computing, programmers must write concurrent code to obtainperformance, much harder than sequential code. Transactions are part of thesolution: they reduce concurrent reasoning to sequential reasoning. Buthigh-performance data structures require relaxed transactional memorytechniques like open nesting. This places a tricky correctness burden on theprogrammer: identifying which operations on the data structure conflict(cannot run in simultaneous transactions), and how to undo operations to backout incomplete transactions.The proposed solution is to specify what a data structure ought to do, and toprove that the programmer's conflict and undo specifications are correct. Theproject will complete a proof-of-concept tool to demonstrate the feasibilityof the approach.The intellectual merit includes: a language for specifying data abstractionsas abstract models amenable to the proofs required; a way to describeconflicts between operations on the data type, and undos; a tool to processthe descriptions and build proofs as satisfiability problems; and algorithmsto prove correctness of abstract locking procotols. The project will be moresuccessful than general program proving since it works with abstractions, notimplementations, and it deals with specific properties of interest. Futurework can address correctness of implementation.The broader impact consists in assisting programmers in building safehigh-performance concurrent data structures for multi-core platforms. Thetools and libraries produced will be widely available. Helping solve themulti-core software problem has huge implications for our economy and society.