DURINN: Adversarial Memory and Thread Interleaving for Detecting Durable Linearizability Bugs
DURINN: Adversarial Memory and Thread Interleaving for Detecting Durable Linearizability Bugs
复制标题
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Xinwei Fu;Dongyoon Lee;Changwoo Min
中科院分区：
文献类型：
--
作者：
Xinwei Fu;Dongyoon Lee;Changwoo Min
非易失性内存（NVM）促进了并发崩溃一致数据结构的发展，这些数据结构是各种内存中持久性应用程序的支柱。持久线性化定义了 NVM 支持的并发崩溃一致数据结构的正确语义，其中即使存在崩溃事件，也能保留线性化。然而，设计和实现正确的持久线性化数据结构仍然具有挑战性，因为开发人员需要使用低级缓存刷新和存储栅栏指令手动控制持久性（持久性）。据我们所知，我们提出了 D URINN，这是第一个针对并发 NVM 数据结构的持久线性化检查器。 D URINN 基于对线性化点（当并发数据结构的更改变得公开可见时）和持久性点（当更改变得持久时）之间差距的新颖观察。从详细的差距分析中，我们得出了三种持久线性化错误模式，这些模式使线性化数据结构变得不持久线性化。为了控制巨大的 NVM 状态和线程交错测试空间，D URINN 静态识别可能的线性化点，并主动构建对抗性 NVM 状态和线程交错设置，从而增加揭示持久线性化错误的可能性。 D URINN 从 12 个并发 NVM 数据结构中有效检测到 27 个（15 个新的）持久线性化错误，而没有出现测试空间爆炸问题。从 12 个中检测到持久错误 有 10 个
Non-volatile memory (NVM) has promoted the development of concurrent crash-consistent data structures, which serve as the backbone of various in-memory persistent appli-cations. Durable linearizability defines the correct semantics of NVM-backed concurrent crash-consistent data structures, in which linearizability is preserved even in the presence of a crash event. However, designing and implementing a correct durable linearizable data structure remain challenging as developers are to manually control durability (persistence) using low-level cache flush and store fence instructions. We present D URINN , to the best of our knowledge, the first durable linearizability checker for concurrent NVM data structures. D URINN is based on the novel observation on the gap between linearizability point – when the changes to a concurrent data structure become publicly visible – and durability point – when the changes become persistent. From the detailed gap analysis, we derive three durable linearizability bug patterns that render a linearizable data structure not durable linearizable. To tame the huge NVM states and thread interleaving test space, D URINN statically identifies likely-linearization points and actively constructs adversarial NVM state and thread interleaving settings that increase the likelihood of revealing durable linearizability bugs. D URINN effectively detected 27 (15 new) durable linearizability bugs from 12 concurrent NVM data structures without a test space explosion problem. durable bugs were detected from 12 There 10