一句话：提出通用、模块化、增量的证明技术，用于建立持久并发数据结构的持久线性化。
持久并发数据结构需在掉电或崩溃后恢复一致状态，其正确性通常由持久线性化（DL）刻画：操作须原子地按实时顺序执行，且恢复状态须对应该顺序的某个前缀。然而形式化DL证明极少，现有工作仅覆盖简单持久算法与特定简化持久模型。本文提出一种通用、强大、模块化且增量的DL证明技术：不绑定具体持久或一致性模型，可复用已有线性化论证，建立DL所需的额外条件随算法复杂度变化。作者在持久集合的多个版本上展示该技术，并覆盖 Zuriel 等人的 link-free set。
There is an increasing body of literature proposing new and efficient persistent versions of concurrent data structures ensuring that a consistent state can be recovered after a power failure or a crash. Their correctness is typically stated in terms of durable linearizability (DL), which requires that individual library operations appear to be executed atomically in a sequence consistent with the real-time order and, moreover, that recovering from a crash return a state corresponding to a prefix of that sequence. Sadly, however, there are hardly any formal DL proofs, and those that do exist cover the correctness of rather simple persistent algorithms on specific (simplified) persistency models. In response, we propose a general, powerful, modular, and incremental proof technique that can be used to guide the development and establish DL. Our technique is (1) general , in that it is not tied to a specific persistency and/or consistency model, (2) powerful , in that it can handle the most advanced persistent algorithms in the literature, (3) modular , in that it allows the reuse of an existing linearizability argument, and (4) incremental , in that the additional requirements for establishing DL depend on the complexity of the algorithm to be verified. We illustrate this technique on various versions of a persistent set, leading to the link-free set of Zuriel et al.
@article{paperbot2058,
title = {The Path to Durable Linearizability},
author = {Emanuele D'Osualdo and Azalea Raad and Viktor Vafeiadis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571219}
}