A Fully Verified Persistency Library

Non-volatile memory (NVM) technologies offer DRAM-like speeds with the added benefit of failure resilience. However, developing concurrent programs for NVM can be challenging since programmers must consider both inter-thread synchronisation and durability aspects at the same time. To alleviate this, libraries such as FliT have been developed to manage transformations to durability, allowing a linearizable concurrent object to be converted into a durably linearizable one by replacing the reads/writes to memory by calls to corresponding operations of the FliT library. However, a formal proof of correctness for FliT is missing, and standard proof techniques for durable linearizability are challenging to apply, since FliT itself is not durably linearizable. In this paper, we study the problem of proving correctness of transformations to durability. First, we develop an abstract persistency library (called PLib) that operationally characterises transformations to durability. We prove soundness of PLib via a forward simulation coupled with a prophecy variable used as an oracle about future behaviour. Second, we show correctness of the library FliT by proving that FliTrefines PLib under the realistic PTSO memory model, i.e., the persistent version of TSO memory model implemented by Intel architectures. The proof of refinement between FliT and PLib has been mechanised within the theorem prover KIV. Taken together, these proofs guarantee that FliT is also sound wrt transformations to durability.