一句话：首个面向弱持久内存模型的并发分离逻辑，并在 Coq 中机器化验证持久数据结构的崩溃安全与线程安全。
弱持久内存（非易失内存）提供了快速、可按字节寻址的持久主存，围绕它已发展出大量算法与库，但相应的程序验证手段严重缺失。本文提出 Spirea——首个用于弱持久内存模型下程序验证的并发分离逻辑。Spirea 建立在 Iris 与 Perennial 验证框架之上，通过融合二者的特性并引入新技术，支持对崩溃安全与线程安全程序及库进行高层的模块化推理。该逻辑在 Coq 证明助手中完全机器化，并支持使用 Iris Proof Mode 进行交互式证明开发。作者用 Spirea 验证了若干带有模块化规约的挑战性实例，展示了其能够验证支持空恢复（null-recovery）的非阻塞持久数据结构的线程安全与崩溃安全，特别是适配持久内存的 Treiber 栈与 Michael-Scott 队列。这是首次使用程序逻辑验证持久数据结构。
Weak persistent memory (a.k.a. non-volatile memory) is an emerging technology that offers fast byte-addressable durable main memory. A wealth of algorithms and libraries has been developed to explore this exciting technology. As noted by others, this has led to a significant verification gap. Towards closing this gap, we present Spirea, the first concurrent separation logic for verification of programs under a weak persistent memory model. Spirea is based on the Iris and Perennial verification frameworks, and by combining features from these logics with novel techniques it supports high-level modular reasoning about crash-safe and thread-safe programs and libraries. Spirea is fully mechanized in the Coq proof assistant and allows for interactive development of proofs with the Iris Proof Mode. We use Spirea to verify several challenging examples with modular specifications. We show how our logic can verify thread-safety and crash-safety of non-blocking durable data structures with null-recovery, in particular the Treiber stack and the Michael-Scott queue adapted to persistent memory. This is the first time durable data structures have been verified with a program logic.
@article{paperbot1838,
title = {Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory},
author = {Simon Friis Vindum and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622820}
}