Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part II
Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part II
复制标题
验证、模型检查和摘要解释 - 第 25 届国际会议，VMCAI 2024，英国伦敦，2024 年 1 月 15-16 日，会议记录，第二部分
DOI：
10.1007/978-3-031-50521-8_2
复制
发表时间：
2024
期刊：
影响因子：
--
通讯作者：
Bodenmüller S
中科院分区：
文献类型：
--
作者：
Bodenmüller S
非易失性存储器(NVM)技术提供了类似DRAM的速度，并增加了故障恢复能力。然而，为NVM开发并发程序可能是具有挑战性的，因为程序员必须同时考虑线程间同步和持久性方面。为了缓解这一问题，已经开发了诸如flit之类的库来管理到持久性的转换，允许通过调用flit库的相应操作来替换对存储器的读/写来将可线性化的并发对象转换为可持久线性化的对象。然而，对于flit的正确性的形式证明是缺失的，并且用于持久线性化的标准证明技术的应用是具有挑战性的，因为它本身不是持久线性化的。在这篇文章中，我们研究了证明持久性变换正确性的问题。首先，我们开发了一个抽象持久性库(称为)，它在操作上表征了从转换到持久性的转换。我们通过一个正向模拟和一个预言变量来证明的可靠性，该预言变量被用来预测未来的行为。其次，我们通过证明FliTrees在现实存储模型下，即Intel体系结构实现的TSO存储模型的持久版本下，证明了库flit的正确性。Flit和之间的精化证明已经在定理证明器KIV中实现了机械化。综上所述，这些证明保证了WRT向耐久性的转变也是合理的。
Non-volatile memory (NVM) technologies offer DRAM-like speeds with the added benefit of failure resilience. However, developing concurrent programs for NVM can be challenging since programmers must consider both inter-thread synchronisation and durability aspects at the same time. To alleviate this, libraries such as FliT have been developed to managetransformations to durability, allowing a linearizable concurrent object to be converted into a durably linearizable one by replacing the reads/writes to memory by calls to corresponding operations of the FliT library. However, a formal proof of correctness for FliT is missing, and standard proof techniques for durable linearizability are challenging to apply, sinceitself is not durably linearizable. In this paper, we study the problem of proving correctness of transformations to durability. First, we develop an abstractpersistency library(called) that operationally characterises transformations to durability. We prove soundness ofvia a forward simulation coupled with aprophecy variableused as an oracle about future behaviour. Second, we show correctness of the library FliT by proving that FliTrefinesunder the realisticmemory model, i.e., the persistent version of TSO memory model implemented by Intel architectures. The proof of refinement between FliT andhas been mechanised within the theorem prover KIV. Taken together, these proofs guarantee thatis also sound wrt transformations to durability.