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

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.