A Test Suite for Model Checking Persistent Memory Programs

Abstract

The latest advances in memory technologies have brought Persistent Memory to the spotlight. Persistent Memory (PM) provides DRAM-like performance and byte-addressability, while preserving its content in case of a crash (non-volatility). To ensure correctness of programs targeting PM, memory architectures, like Intel’s x86, have introduced new instructions that flush the contents of the volatile caches to the persistent domain. These instructions induce certain persist orderings, which are formalized by persistency memory models and define the allowed behaviours of the system after a crash. This thesis develops a test suite for PM programs, consisting of both litmus and data structure tests. Litmus tests aim to check the sanity of the tool used for verification. In our case, we used PERSEVERE, which is a persistency model checking tool under current development. Through our tests, we were able to pinpoint an internal inability of PERSEVERE to support the Px86 memory model, which led its developers to provide additional support in the tool’s core. The data structure tests try to test various implementations of lock-free data structures, as well as some adaptations and transformations found in recent literature that turn these implementations into durable linearizable ones. With our test suite, we were able to check that the original implementations of these data structures were not durably linearizable. On the other hand, the durable versions of the data structures pass our checks. Furthermore, we experimented with eliminating explicit flush instructions in these versions, which led to durably linearizability violations and therefore proving the necessity of these instructions to ensure durable linearizability. Our test suite can be used as a guideline for how to use model checking to verify durable data structures and persistent libraries, and can serve as a benchmark for persistency model checking tools.