Software Engineering and Formal Methods - 19th International Conference, SEFM 2021, Virtual Event, December 6-10, 2021, Proceedings
Software Engineering and Formal Methods - 19th International Conference, SEFM 2021, Virtual Event, December 6-10, 2021, Proceedings
复制标题
软件工程和形式化方法 - 第 19 届国际会议，SEFM 2021，虚拟活动，2021 年 12 月 6-10 日，会议记录
DOI：
10.1007/978-3-030-92124-8_13
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Dongol B
中科院分区：
文献类型：
--
作者：
Dongol B
软件事务存储器（STM）是一种支持软件的事务存储器形式，通常实现为语言库，代表程序员提供细粒度的并发控制。STM算法最近已经被调整以科普非易失性存储器（NVM），也称为持久性存储器，这是存储器的新范例，其即使在断电之后也保留其内容。本文提出了一种利用FDR（a model checker forspecifications）验证STM算法正确性的模型检测方法。我们的证据是基于操作事务内存规范，允许证明（持久）不透明性，在易失性和持久性内存下的STM的主要安全属性，通过细化进行验证。由于FDR使自动证明的细化，我们得到了一个自动检查的STM算法的有界模型的不透明度和持久的不透明度的技术。
Software transactional memory (STMs) is a software-enabled form of transactional memory, typically implemented as a language library, that provides fine-grained concurrency control on behalf of a programmer. STM algorithms have been recently adapted to cope with non-volatile memory (NVM), aka persistent memory, which is a new paradigm for memory that preserves its contents even after power loss. This paper presents a model checking approach to validating correctness of STM algorithms using FDR (a model checker forspecifications). Our proofs are based on operational transactional memory specifications that allow proofs of (durable) opacity, the main safety property for STMs under volatile and persistent memory, to be verified by refinement. Since FDR enables automatic proofs of refinement, we obtain an automatic technique for checking both opacity and durable opacity of bounded models of STM algorithms.