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 \(\textsf{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 \(\textsf{PLib} \) ) that operationally characterises transformations to durability. We prove soundness of \(\textsf{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 FliT refines \(\textsf{PLib} \) under the realistic \(\textsf{PTSO} \) memory model, i.e., the persistent version of TSO memory model implemented by Intel architectures. The proof of refinement between FliT and \(\textsf{PLib} \) has been mechanised within the theorem prover KIV. Taken together, these proofs guarantee that \(\textsf{FliT} \) is also sound wrt transformations to durability.