一句话：将 Intel-x86 一致性/持久性语义扩展到非临时写、不可缓存、写合并和写穿内存类型，并证明操作式与声明式模型等价。
现有 Intel-x86 语义形式化只覆盖多线程一致性及与非易失内存交互的持久性语义相关特性的一小部分。本文扩展这些形式化，纳入非临时写（提供更高性能并用于确保更新刷回内存）、对不可缓存、写合并和写穿等其他 Intel-x86 内存类型的读写，以及这些特性之间的交互。作者以操作式和声明式两种风格建立形式模型，并证明两种刻画等价。最后，通过对不同 Intel-x86 实现开展大量测试，对所扩展的一致性语义及其微妙交互进行经验验证。
Existing semantic formalisations of the Intel-x86 architecture cover only a small fragment of its available features that are relevant for the consistency semantics of multi-threaded programs as well as the persistency semantics of programs interfacing with non-volatile memory. We extend these formalisations to cover: (1) non-temporal writes, which provide higher performance and are used to ensure that updates are flushed to memory; (2) reads and writes to other Intel-x86 memory types, namely uncacheable, write-combined, and write-through; as well as (3) the interaction between these features. We develop our formal model in both operational and declarative styles, and prove that the two characterisations are equivalent. We have empirically validated our formalisation of the consistency semantics of these additional features and their subtle interactions by extensive testing on different Intel-x86 implementations.
@article{paperbot1593,
title = {Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores},
author = {Azalea Raad and Luc Maranget and Viktor Vafeiadis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498683}
}