模块化验证持久性不透明性
Modularising Verification Of Durable Opacity
AI总结：
本文提出持久性不透明性作为STM在非易失性内存下的正确性条件，开发了NOrec的持久性版本，并通过分离持久性与不透明性证明实现模块化验证。
摘要：
非易失性内存（NVM），也称为持久性内存，是一种新兴的内存范式，即使在断电后也能保留其内容。NVM被广泛预期将变得无处不在，硬件架构已经为NVM编程提供支持。这激发了人们对设计新概念的兴趣，以确保并发编程抽象在面对持久性时的正确性，并推动了相关验证方法的发展。软件事务性内存（STM）是一种关键的编程抽象，支持对共享状态的并发访问。类似于线性化作为并发数据结构的正确性条件，STM有一个公认的正确性概念，称为不透明性。我们最近提出了持久性不透明性，作为不透明性在非易失性内存环境中的自然扩展。连同这一新颖的正确性条件，我们设计了一种基于精化的验证技术。在本文中，我们从两个方向扩展这项工作。首先，我们开发了NOrec（无所有权记录）的持久性不透明版本，这是一种已被证明不透明的现有STM算法。其次，我们通过将内存访问的持久性证明与不透明性证明分离，来模块化我们现有的验证方法。对于NOrec，这使我们能够重用现有的不透明性证明，并辅以对共享状态访问的持久性证明。
英文摘要：
Non-volatile memory (NVM), also known as persistent memory, is an emerging paradigm for memory that preserves its contents even after power loss. NVM is widely expected to become ubiquitous, and hardware architectures are already providing support for NVM programming. This has stimulated interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistency and in the development of associated verification approaches. Software transactional memory (STM) is a key programming abstraction that supports concurrent access to shared state. In a fashion similar to linearizability as the correctness condition for concurrent data structures, there is an established notion of correctness for STMs known as opacity. We have recently proposed durable opacity as the natural extension of opacity to a setting with non-volatile memory. Together with this novel correctness condition, we designed a verification technique based on refinement. In this paper, we extend this work in two directions. First, we develop a durably opaque version of NOrec (no ownership records), an existing STM algorithm proven to be opaque. Second, we modularise our existing verification approach by separating the proof of durability of memory accesses from the proof of opacity. For NOrec, this allows us to re-use an existing opacity proof and complement it with a proof of the durability of accesses to shared state.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
