Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8
Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8
复制标题
DOI：
10.1145/3453483.3454027
复制
发表时间：
2021-06
期刊：
影响因子：
--
通讯作者：
K. Cho;Sung-Hwan Lee;Azalea Raad;Jeehoon Kang
中科院分区：
文献类型：
--
作者：
K. Cho;Sung-Hwan Lee;Azalea Raad;Jeehoon Kang
非易失性存储器（NVM）是一种尖端的存储技术，它保证了DRAM的性能和SSD的耐用性。最近的工作为Intel-x86和Armv 8等主流架构提出了几种持久性模型，描述了写入传播到NVM的顺序。但是，这些模型有几个局限性;最明显的是，它们要么缺乏操作模型，要么不支持持久同步模式。我们通过改进现有的持久化模型来缩小这一差距。首先，受近期语义研究的启发，提出了一种统一的操作风格，用于使用视图描述持久化，并为Intel-x86和Armv 8开发了基于视图的操作持久化模型，从而给出了Armv 8持久化的第一个操作模型。接下来，我们提出了一个统一的公理风格来描述硬件持久化，允许我们重铸和修复现有的Intel-x86和Armv 8持久化的公理模型。我们证明了我们的公理模型与英特尔和Arm工程师审查的权威语义是等价的。我们进一步证明，每个公理化的硬件持久化模型是等价的，它的操作对应。最后，我们开发了一个持久模型检测算法和工具，并使用它来验证几个有代表性的例子。
Non-volatile memory (NVM) is a cutting-edge storage technology that promises the performance of DRAM with the durability of SSD. Recent work has proposed several persistency models for mainstream architectures such as Intel-x86 and Armv8, describing the order in which writes are propagated to NVM. However, these models have several limitations; most notably, they either lack operational models or do not support persistent synchronization patterns. We close this gap by revamping the existing persistency models. First, inspired by the recent work on promising semantics, we propose a unified operational style for describing persistency using views, and develop view-based operational persistency models for Intel-x86 and Armv8, thus presenting the first operational model for Armv8 persistency. Next, we propose a unified axiomatic style for describing hardware persistency, allowing us to recast and repair the existing axiomatic models of Intel-x86 and Armv8 persistency. We prove that our axiomatic models are equivalent to the authoritative semantics reviewed by Intel and Arm engineers. We further prove that each axiomatic hardware persistency model is equivalent to its operational counterpart. Finally, we develop a persistent model checking algorithm and tool, and use it to verify several representative examples.