Verifying correctness of persistent concurrent data structures: a sound and complete method
Verifying correctness of persistent concurrent data structures: a sound and complete method
复制标题
验证持久并发数据结构的正确性：一种健全且完整的方法
DOI：
10.1007/s00165-021-00541-8
复制
发表时间：
2021
影响因子：
1
通讯作者：
Derrick J
中科院分区：
文献类型：
--
作者：
Derrick J
非易失性存储器(NVM)，又称永久存储器，是一种即使断电也能保存其内容的新存储器范例。预计NVM的普遍存在激发了人们对持久并发数据结构的设计以及相关的正确性概念的兴趣。在本文中，我们提出了第一个形式证明技术的持久线性化，这是一个正确的准则，扩展了线性化处理崩溃和恢复在NVM的背景下。我们的证明是基于并发数据结构的IO自动机表示的精化。为此，我们开发了一个通用过程，用于将任何标准顺序数据结构转换为持久规范。由于持久规范只表现出可持久线性化的行为，因此它在我们的求精证明中充当抽象规范。我们在最近提出的持久内存队列上举例说明了我们的技术，该队列构建在Michael和Scott的无锁队列之上。
Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory preserving its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design ofpersistentconcurrent data structures, together with associated notions of correctness. In this paper, we present the first formal proof technique fordurable linearizability, which is a correctness criterion that extends linearizability to handle crashes and recovery in the context of NVM. Our proofs are based on refinement of IO-automata representations of concurrent data structures. To this end, we develop a generic procedure for transforming any standard sequential data structure into a durable specification. Since the durable specification only exhibits durably linearizable behaviours, it serves as the abstract specification in our refinement proof. We exemplify our technique on a recently proposed persistent memory queue that builds on Michael and Scott’s lock-free queue.
登录
查看更多内容
网络和分布式系统的形式技术 - FORTE 2008，第 28 届 IFIP WG 6.1 国际会议，日本东京，2008 年 6 月 10-13 日，会议记录
DOI：
--
发表时间：
2008
期刊：
Formal Techniques for (Networked and) Distributed Systems
影响因子：
--
作者：
Kenji Suzuki;T. Higashino;K. Yasumoto;K. El
通讯作者：
K. El
DOI：
10.1007/978-3-642-45221-5_9
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Benzmüller C
通讯作者：
Benzmüller C
通过崩溃优化对文件系统进行一键式验证
DOI：
--
发表时间：
2016
期刊：
USENIX Annual Technical Conference
影响因子：
--
作者：
Helgi Sigurbjarnarson;James Bornholt;Nicolas Christin;L. Cranor
通讯作者：
L. Cranor
DOI：
10.1007/978-3-319-46750-4_1
发表时间：
2016
期刊：
影响因子：
--
作者：
Oleg Travkin;Heike Wehrheim
通讯作者：
Heike Wehrheim
影响因子：
1.8
作者：
Raad, Azalea;Doko, Marko;Vafeiadis, Viktor
通讯作者：
Vafeiadis, Viktor