Towards Model Checking Library for Persistent Data Structures

Persistent concurrent data structures, which allow concurrent access and store critical data into byte-addressable non-volatile memory (NVM) to keep them beyond system crashes, are attractive. However, they are complicated and hard to be confident in the correctness of them because 1) cache and registers are expected to remain volatile, and 2) cache flush instructions are reordered with load and store instructions in accordance with the memory model of the system. This paper provides a design of a model checking library, named MMLib-NVM, which is useful to verify persistent concurrent data structures that run on hardware with a weak memory model and non-volatile memory. The library is for the SPIN model checker. MMLib-NVM allows the users to develop models of their data structures without considering the memory model and behaviour of NVM, besides explicit memory barriers and cache flush instructions. We implemented a prototype of MMLib-NVM and investigated a property derived from durable linearisability of a persistent lock-free queue, the durable queue, of Friedman et al. against the sequential consistency and total store ordering memory models by model checking using MMLib-NVM.