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.

翻译：我们提出了一个通用框架，用于指定和验证持久化库，即在其执行机器发生故障时提供某种持久性保证的数据结构库。该框架支持对单个库的正确性进行模块化推理（水平与垂直组合性），并且足够通用，能够涵盖所有现有的持久化库规范，从硬件架构规范到持久线性化等正确性条件。作为案例研究，我们在该框架内指定了FliT和Mirror库，验证了它们在Px86上的实现，并利用它们构建了更高层次的持久线性化库。此外，我们还指定并验证了一个持久化事务库，该库突显了持久内存相对于弱内存所特有的技术挑战，以及我们的框架如何应对这些挑战。