Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
复制标题
DOI：
10.1007/978-3-030-50086-3_3
复制
发表时间：
2020-05-13
期刊：
影响因子：
--
通讯作者：
Wehrheim H
中科院分区：
文献类型：
--
作者：
Bila E;Doherty S;Dongol B;Derrick J;Schellhorn G;Wehrheim H
非挥发性内存（NVM）（又名持久记忆）是一种新的内存范式，即使在功率损失后，也可以保留其内容。 NVM的预期无处不在，激发了对新颖概念的设计的兴趣，从而确保了面对持久性的并发编程抽象的正确性。到目前为止，这导致了许多持续的并发数据结构的设计，这些数据结构构建是为了满足相关的正确性概念：持久的线性化性。
在本文中，我们将耐用的并发正确性的原理转移到软件交易记忆（STM）的区域。软件交易内存算法允许同时访问共享状态。与并发数据结构的线性化性一样，不透明度是STM的正确性概念。首先，我们提供了耐用的不透明度的新颖定义，该定义扩展了不透明度，以处理NVM的情况下处理崩溃和恢复。其次，我们开发了现有的STM算法的持久不透明版本，即Transactional Mutex锁（TML）。第三，我们根据TML之间的完善和通过调整TMS2规范的耐用性不透明度表征设计了一种用于耐用性不透明度的证明技术。最后，我们应用了这种证明技术，以表明TML持久版本确实是持久不透明的。正确的证明是在伊莎贝尔内部机械化的。
Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistency. So far, this has lead to the design of a number of persistent concurrent data structures, built to satisfy an associated notion of correctness: durable linearizability. In this paper, we transfer the principle of durable concurrent correctness to the area of software transactional memory (STM). Software transactional memory algorithms allow for concurrent access to shared state. Like linearizability for concurrent data structures, opacity is the established notion of correctness for STMs. First, we provide a novel definition of durable opacity extending opacity to handle crashes and recovery in the context of NVM. Second, we develop a durably opaque version of an existing STM algorithm, namely the Transactional Mutex Lock (TML). Third, we design a proof technique for durable opacity based on refinement between TML and an operational characterisation of durable opacity by adapting the TMS2 specification. Finally, we apply this proof technique to show that the durable version of TML is indeed durably opaque. The correctness proof is mechanized within Isabelle.
登录
查看更多内容
影响因子：
1.3
作者：
HERLIHY, MP;WING, JM
通讯作者：
WING, JM
影响因子：
--
作者：
Chakrabarti, Dhruva R.;Boehm, Hans-J.;Bhandari, Kumud
通讯作者：
Bhandari, Kumud
影响因子：
1
作者：
Doherty, Simon;Groves, Lindsay;Moir, Mark
通讯作者：
Moir, Mark
影响因子：
--
作者：
Izraelevitz, Joseph;Kelly, Terence;Kolli, Aasheesh
通讯作者：
Kolli, Aasheesh
影响因子：
1
作者：
LYNCH, N;VAANDRAGER, F
通讯作者：
VAANDRAGER, F