EAGER: Automating Correctness Proofs of Transactionalized Data Structures

在多核计算中，程序员必须编写并发代码来获得性能，这比顺序代码要难得多。事务是解决方案的一部分：它们将并发推理简化为顺序推理。但高性能的数据结构需要宽松的事务内存技术，如开放嵌套。这给程序员带来了棘手的正确性负担：识别数据结构上的哪些操作发生冲突(不能在同时事务中运行)，以及如何撤消操作以取消未完成的事务。提出的解决方案是指定数据结构应该做什么，并证明程序员的冲突和撤消规范是正确的。该项目将完成一个概念验证工具，以演示该方法的可行性。智能优势包括：用于将数据抽象指定为服从所需证明的抽象模型的语言；描述数据类型操作和撤消之间的冲突的方法；处理描述并作为可满足性问题建立证明的工具；以及证明抽象锁定协议的正确性的算法。该项目将比一般的程序证明更成功，因为它与抽象、非实现一起工作，并且它处理感兴趣的特定属性。FutureWork可以解决实现的正确性。更广泛的影响在于帮助程序员为多核平台构建安全高性能的并发数据结构。制作的工具和库将广泛使用。帮助解决多核软件问题对我们的经济和社会具有巨大的影响。

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.