一句话：为 x86-TSO 非易失内存建立等价持久性模型，并给出到 x86 的健全映射与数据竞争自由保证。
论文研究 x86-TSO 体系结构下非易失内存的形式语义。作者证明 Raad 等人 POPL'20 模型中显式 persist 操作虽只强制非易失内存写之间的顺序，但从可达状态看等价于要求此前写真正落入非易失内存的模型，从而给出更贴近开发者直觉的新模型。进一步提出更简单更强的顺序一致持久性模型，构造到 x86 的健全映射，并建立数据竞争自由保证，为程序员提供安全编程规范。操作模型配有等价声明式表述，便于形式论证，也可用于 x86 持久性下的程序验证。
We study the formal semantics of non-volatile memory in the x86-TSO architecture. We show that while the explicit persist operations in the recent model of Raad et al. from POPL'20 only enforce order between writes to the non-volatile memory, it is equivalent, in terms of reachable states, to a model whose explicit persist operations mandate that prior writes are actually written to the non-volatile memory. The latter provides a novel model that is much closer to common developers' understanding of persistency semantics. We further introduce a simpler and stronger sequentially consistent persistency model, develop a sound mapping from this model to x86, and establish a data-race-freedom guarantee providing programmers with a safe programming discipline. Our operational models are accompanied with equivalent declarative formulations, which facilitate our formal arguments, and may prove useful for program verification under x86 persistency.