SHF: Small: PMChecker: Tool Support for Crash-Consistent Persistent Memory Programs

英特尔的Optane Memory等新型永久存储技术的商业化应用有望改变程序存储和操作数据的方式。实现永久存储器的好处的一个主要挑战是确保软件可以在系统崩溃的情况下幸免于难，而不会损坏存储在永久存储器中的数据。简单地直接测试持久性内存软件是不可行的：暴露持久性错误需要精确定时的电源故障或崩溃和正确的缓存状态的组合。该项目的新颖性是(1)开发了一种新的模型检查持久化内存程序的方法，该方法可以找到持久化错误并扩展到真实世界的代码，(2)开发了形式正确性模型，可以确保代码正确地持久化数据结构，(3)开发了一个可以识别现实代码中的持久化错误的工具，以及(4)开发了一个可以自动生成必要指令来持久化数据的工具。该项目的影响是，它正在创造工具，帮助行业构建可靠的软件，利用新兴的持久存储器技术。该项目借鉴并发数据结构的工作经验，为持久存储器程序开发适当的正确性概念。这些概念足够强大，足以确保永久内存程序正确地将数据从缓存刷新到永久内存。该项目开发了一个模型检查器，其中包括一个自动分析，以检查与这些正确性概念相关的持久性内存程序。这种分析可以帮助开发人员找到持久性内存程序中的静默错误，并将错误定位到特定的代码区域。最后，该项目建立在这一分析的基础上，以实现刷新操作的自动合成，以帮助开发人员为持久存储器创建崩溃一致性软件。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

The commercial availability of new persistent-memory technologies such as Intel's Optane memory promises to transform how programs store and manipulate data. A major challenge in realizing the benefits of persistent memory is ensuring that software can survive system crashes without corrupting data that is stored in persistent memory. Simply directly testing persistent-memory software is not feasible: exposing persistency bugs requires a combination of a precisely timed power failure or crash and the correct cache state. The project’s novelties are (1) the development of a new approach to model-checking persistent-memory programs that can find persistency bugs and scale to real world code, (2) the development of formal correctness models that can ensure that code correctly persists data structures, (3) the development of a tool that can identify persistency bugs in real world code, and (4) the development of a tool that can automatically generate the necessary instructions to persist data. The project’s impacts are that it is creating tools that help industry build reliable software that takes advantage of emerging persistent memory technologies.This project develops appropriate notions of correctness for persistent-memory programs borrowing ideas from work in concurrent data structures. These notions are sufficiently strong to ensure that persistent-memory programs correctly flush data from caches to persistent memory. The project develops a model checker that includes an automated analysis to check persistent-memory programs with respect to these correctness notions. This analysis can help developers both find silent bugs in persistent-memory programs and to localize a bug to a specific region of code. Finally, the project builds on this analysis to enable the automated synthesis of flush operations to assist developers in creating crash-consistent software for persistent memory.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.