“How can one check a large routine in the sense of making sure that it’s right? The programmer should make a number of definite assertions which can be checked individually, and from which the correctness of the whole program easily follows.” – Alan Turing
Programming for persistent memory is hard
Persistent memory unifies the functionality of memory and storage by levering fast, byte-addressable, non-volatile memory technologies. It enables the software to bypass OS indirections and directly update persistent data in-place in memory, significantly improving performance over the conventional systems. However, it also comes with the challenge of providing efficient system support, which traditionally, was the responsibility of the file system. Persistent data is expected to be recoverable in the event of a crash (e.g., power failure). Now, persistent memory applications need to provide support for crash consistency at the application level instead of relying on the file system.
There are two fundamental requirements for ensuring crash consistency: durability and ordering. A durability guarantee from the persistent memory system is required to enforce that data reliably reach persistence. Unfortunately, simply executing a store instruction to a persistent memory location does not ensure the update has become persistent because of the volatile cache hierarchies in our current systems. As a solution, the x86 ISA introduced new optimized instructions (e.g., clwb) to efficiently writeback cache lines to memory, and ARM introduced DC CVAP to writeback a cache line to the persistence domain.
Enforcing ordering is another fundamental necessity to ensure crash consistency. An ordering guarantee from the persistent memory system is required to explicitly order persistent operations as the hardware can reorder instructions in the processor and in the memory hierarchy. For example, the commonly used undo logging mechanism requires the undo log entry to be created and persisted before the associated data gets modified. The x86 ISA provides ordering guarantees through the sfence instruction. A combination of a clwb and an sfence instructions issued after a write to a cache line ensures that the new value of the cache line has persisted before any subsequent writes.
The problem of using these low-level primitives to enforce durability and ordering guarantees is that the program order of instructions does not remain the same during the execution. The programmers can not verify that the order of persist operations executed in the hardware is actually what they intended in the program. Even with the help of transactional libraries that build upon these low-level primitive (e.g., Intel’s PMDK), programmers still need to understand the specification of the durability and ordering guarantees provided by these libraries to properly use them. As a result, programmers cannot determine whether the crash consistency algorithm is correctly implemented, i.e., whether the specified order will not result in a runtime order that violates the required persistent ordering.
Fences and writeback operations do not provide an intuitive interface for programmers to reason about (i) whether a memory location/object has persisted, and (ii) the order in which different memory locations/objects can persist during runtime, the two fundamental requirements to reason about crash consistency. The goal of PMTest is to bridge this gap between the program order and runtime order by providing an assertion-like checkers to the software. To this end, PMtest supports two low-level checkers that developers can use for debugging: IsPersist and IsOrderedBefore, that check whether (i) certain persistent objects have been persisted since their last update and (ii) if a certain persistent operation has been ordered before another, enabling testing of the two fundamental properties of any crash consistency. These checkers expose the runtime ordering to the software and PMTest verifies if any of the run time ordering will violate the order programmer is expecting in the code.
On top of that, programmers can use these two low-level checkers to build custom, high-level checkers for different libraries and persistency models. PMTest provides high-level checkers that automates the process of debugging programs built on top of Intel’s transactional library (PMDK). PMTest is also easily extensible for future PM hardware and libraries. Using PMTest, we have detected 3 new bugs in software developed by expert programmers from Intel, including an optimized file system (PMFS) and applications based on the transactional library in PMDK. The codebase of PMTest is available here. We would love to hear your feedback.
Where do we go from here
The goal of PMTest is to assist programmers to write correct software for persistent memory systems. We expect that it will open up new research areas related to rethinking and redesigning the correctness of persistent memory applications. For example, how to formally verify the persistent memory interface, how to perform black-box or grey-box testing that requires zero or little knowledge about the implementation, and how to model system interaction in testing when applications bypass the kernel.
In addition to that, one design principle of PMTest is the awareness of the underlying hardware. It decouples the hardware implementation of the ordering and durability guarantee from the programmers. Therefore, PMTest bridges software testing with architectural innovation, as testing frameworks for persistent memory need to be designed with extensive knowledge of the underlying hardware. We hope that PMTest will inspire future research on co-designing software testing and hardware optimization for persistent memory systems. We have a follow-up work in ASPLOS 2020 on modeling crash-consistent bugs as a cross-failure race. Stay tuned!
Samira Khan is an Assistant Professor at the University of Virginia (UVa). Prior to joining UVa, she was a Post Doctoral Researcher at Carnegie Mellon University, funded by Intel Labs. She leads “ShiftLab” at UVa, motivated to initiate a paradigm shift in the current computing system. Her research group focuses on building an end-to-end system stack support for emerging technologies.