Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores
Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores
复制标题
DOI：
10.1145/3498683
复制
发表时间：
2022-01
影响因子：
--
通讯作者：
Azalea Raad;Luc Maranget;Viktor Vafeiadis
中科院分区：
文献类型：
--
作者：
Azalea Raad;Luc Maranget;Viktor Vafeiadis
Intel-x86体系结构的现有语义形式化仅覆盖其可用特征的一小部分，这些特征与多线程程序的一致性语义以及与非易失性存储器接口的程序的持久性语义相关。我们将这些形式化扩展到：(1)非临时写入，它提供更高的性能并用于确保将更新刷新到内存；(2)对其他Intel-x86内存类型的读取和写入，即不可缓存、写入组合和直写；以及(3)这些功能之间的交互。我们开发了操作型和声明型两种形式的模型，并证明了这两种特征是等价的。通过对不同的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.