Specifying and Verifying Persistent Libraries

TL;DR

This paper introduces a comprehensive framework for specifying and verifying persistent libraries, enabling modular reasoning and covering various specifications from hardware to correctness conditions like durable linearizability.

Contribution

It provides a general, modular framework for specifying and verifying persistent libraries, including case studies on real libraries and handling persistent memory challenges.

Findings

Successfully specified and verified FliT and Mirror libraries

Built higher-level durably linearizable libraries within the framework

Addressed technical challenges specific to persistent memory

Abstract

We present a general framework for specifying and verifying persistent libraries, that is, libraries of data structures that provide some persistency guarantees upon a failure of the machine they are executing on. Our framework enables modular reasoning about the correctness of individual libraries (horizontal and vertical compositionality) and is general enough to encompass all existing persistent library specifications ranging from hardware architectural specifications to correctness conditions such as durable linearizability. As case studies, we specify the FliT and Mirror libraries, verify their implementations over Px86, and use them to build higher-level durably linearizable libraries, all within our framework. We also specify and verify a persistent transaction library that highlights some of the technical challenges which are specific to persistent memory compared to weak memory and how they are handled by our framework.