paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Memento: A Framework for Detectable Recoverability in Persistent Memory

Memento:持久内存中可检测可恢复性的框架
PLDI 7(PLDI)2023匹配度 2/10 · 该论文研究持久内存并发数据结构及其可检测可恢复性,并给出形式化证明,属于PL/系统与程序验证方向;但它不涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,与用户画像中“PL↔AI”及浮点/贝叶斯交叉方向基本无关。引用 4 inbox
Kyeongmin Cho, Seungmin Jeon, Azalea Raad, Jeehoon Kang
crossref: 2026-09-10

AI 速览

一句话:Memento 是一个面向持久内存并发数据结构的通用高性能框架,用时间戳恢复策略实现可检测可恢复性并给出形式化证明。

持久内存(PM)兼具 DRAM 性能与 SSD 持久性,其上并发数据结构(DS)的可检测可恢复性要求同时满足线程安全与崩溃一致性。现有设计可检测可恢复并发 DS 的方法要么局限于简单算法,要么运行时开销过高。本文提出 Memento:一个通用且高性能的编程框架。为保证通用性,Memento 支持 checkpoint、compare-and-swap 等原语操作及其与控制结构的组合;为保证高性能,它采用基于时间戳的恢复策略,相比已有方法需要更少的 PM 写入与 flush。作者形式化证明了 Memento 在崩溃场景下可保证可检测可恢复性。评估方面,作者用 Memento 实现了无锁栈、链表、队列、哈希表以及 combining queue,在压力测试中可从随机崩溃中可检测地恢复,性能与已有手工调优的持久 DS(无论是否支持可检测可恢复性)相当。

问题
如何为持久内存上的并发数据结构提供通用且高性能的可检测可恢复性(同时保证线程安全与崩溃一致性),现有方法要么仅适用于简单算法,要么运行时开销高。
方法
Memento 框架提供 checkpoint、compare-and-swap 等原语及其与控制结构的组合以保证通用性,并采用基于时间戳的恢复策略以减少对持久内存的写入与 flush。
评估
作者形式化证明了 Memento 在崩溃下保证可检测可恢复性,并用其实现了无锁栈、链表、队列、哈希表和 combining queue,通过压力测试中的随机崩溃恢复进行验证,性能与已有手工调优的持久数据结构相当。
原文摘要(Abstract)

Persistent memory (PM) is an emerging class of storage technology that combines the performance of DRAM with the durability of SSD, offering the best of both worlds. This had led to a surge of research on persistent objects in PM. Among such persistent objects, concurrent data structures (DSs) are particularly interesting thanks to their performance and scalability. One of the most widely used correctness criteria for persistent concurrent DSs is detectable recoverability , ensuring both thread safety (for correctness in non-crashing concurrent executions) and crash consistency (for correctness in crashing executions). However, the existing approaches to designing detectably recoverable concurrent DSs are either limited to simple algorithms or suffer from high runtime overheads. We present Memento: a general and high-performance programming framework for detectably recoverable concurrent DSs in PM. To ensure general applicability to various DSs, Memento supports primitive operations such as checkpoint and compare-and-swap and their composition with control constructs. To ensure high performance, Memento employs a timestamp-based recovery strategy that requires fewer writes and flushes to PM than the existing approaches. We formally prove that Memento ensures detectable recoverability in the presence of crashes. To showcase Memento, we implement a lock-free stack, list, queue, and hash table, and a combining queue that detectably recovers from random crashes in stress tests and performs comparably to existing hand-tuned persistent DSs with and without detectable recoverability.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1976,
  title = {Memento: A Framework for Detectable Recoverability in Persistent Memory},
  author = {Kyeongmin Cho and Seungmin Jeon and Azalea Raad and Jeehoon Kang},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {PLDI},
  year = {2023},
  doi = {10.1145/3591232}
}