Model Checking Buffered Durable Linearizability in CSP

doi:10.1007/978-3-032-10794-7_7

Model Checking Buffered Durable Linearizability in CSP

2026-01-01

0

PRE

AI

DOI：10.1007/978-3-032-10794-7_7

原文链接

原文求助

摘要

En 中文

非易失性存储器（NVM）是一种高性能存储技术，可在系统崩溃（例如断电）时支持数据的持久性（即耐久性）。对于并发对象（例如并发数据结构如栈和哈希映射）的实现，NVM提出了正确性问题：崩溃后实现能否恢复到一致状态并继续执行？本文研究了一种针对周期性持久并发对象实现的正确性概念，即缓冲持久线性化，并开发了一种基于精化的证明方法用于缓冲持久线性化。为了支持我们的证明，我们开发了一种通用的抽象规范，用于缓冲持久线性化对象，该规范是从对象的顺序规范生成的。我们的主要案例研究是一种名为Dali的并发哈希映射，我们证明它满足缓冲持久线性化。具体来说，我们使用基于CSP的模型检测器FDR，它提供了一种完全自动化的方法来检查迹精化。

Keyword:

non-volatile memory

concurrent objects

buffered durable linearizability

model checking

CSP

Model Checking Buffered Durable Linearizability in CSP

摘要

期刊

机构