一句话：首次形式化 Intel-x86 的持久性语义 Px86，给出操作式与声明式定义并证明二者等价。
新兴非易失内存技术有望兼具磁盘持久性与 RAM 性能，已有多种内存持久性模型，但广泛使用的 x86 架构的持久性语义此前未被研究。本文提出 Px86 模型，首次形式化 Intel-x86 的持久性语义；分别给出操作式与声明式刻画，并证明二者等价。为展示 Px86 的可用性，作者在其上开发了持久事务库和 Michael–Scott 队列的持久变体，并将声明式模型编码到 Alloy 中，用来自动生成持久性 litmus 测试。该工作为 x86 非易失内存编程提供了形式化基础与测试工具。
Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of RAM. To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, the persistency semantics of the ubiquitous x86 architecture remains unexplored to date. To close this gap, we develop the Px86 (‘persistent x86’) model, formalising the persistency semantics of Intel-x86 for the first time. We formulate Px86 both operationally and declaratively, and prove that the two characterisations are equivalent. To demonstrate the application of Px86, we develop two persistent libraries over Px86: a persistent transactional library, and a persistent variant of the Michael–Scott queue. Finally, we encode our declarative Px86 model in Alloy and use it to generate persistency litmus tests automatically.
@article{paperbot540,
title = {Persistency semantics of the Intel-x86 architecture},
author = {Azalea Raad and John Wickerson and Gil Neiger and Viktor Vafeiadis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371079}
}