耐久不透明性的模块化验证
摘要：非易失性存储器 (NVM)，也称为持久性存储器，是一种新兴的存储器范式，即使在断电后也能保持其内容。NVM被广泛预计将无处不在，并且硬件架构已经提供了对NVM编程的支持。这激发了对在面对持久性时确保并发编程抽象正确性的新概念设计的兴趣，并且对相关的验证方法的开发。 软件事务内存 (STM) 是一种支持并发访问共享状态的关键编程抽象。类似于线性化是并发数据结构的正确性条件，已经确立了透明性作为STM的正确性概念。我们最近提出了持久透明性作为透明性在非易失性存储器环境下的自然扩展。随着这个新的正确性条件，我们设计了一种基于细化的验证技术。在本文中，我们将这项工作沿两个方向进行了扩展。首先，我们为NOrec (无拥有记录) 这个现有的被证明为透明的STM算法开发了一个持久透明版本。其次，我们通过将内存访问的持久性证明与透明性证明分离，将我们现有的验证方法模块化。对于NOrec，这使我们可以重用现有的透明性证明，并通过对共享状态的访问持久性进行证明来补充它。
作者：Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim
论文ID：2011.15013
分类：Distributed, Parallel, and Cluster Computing
分类简称：cs.DC
提交时间：2023-06-22