一句话：提出 CrashLang 语言与类型系统，保证良类型数据结构实现崩溃一致，并实现编译器验证五个基准。
持久内存、CXL 内存共享等技术使数据可跨越崩溃事件，但如何保证崩溃后数据仍一致且可安全访问仍是难题；已有工具多用于找 bug，无法保证程序崩溃一致。本文提出 CrashLang 语言及其类型系统，利用 commit-store 模式：单个存储操作在逻辑上提交整个数据结构操作，从而通过类型系统静态保证良类型实现具有崩溃一致性。作者证明了良类型程序的崩溃一致性，并实现 CrashLang 编译器原型。评估覆盖 Harris 链表、Treiber 栈、Michael-Scott 队列、RCU 二叉搜索树和 Cache-Line 哈希表五个基准，实验验证各实现均能在崩溃后正确存活。
Compute Express Link (CXL) memory sharing, persistent memory, and other related technologies allow data to survive crash events. A key challenge is ensuring that data is consistent after crashes such that it can be safely accessed. While there has been much work on bug-finding tools for persistent memory programs, these tools cannot guarantee that a program is crash-consistent. In this paper, we present a language, CrashLang , and its type system, that together guarantee that well-typed data structure implementations written in CrashLang are crash-consistent. CrashLang leverages the well-known commit-store pattern in which a single store logically commits an entire data structure operation. In this paper, we prove that well-typed CrashLang programs are crash-consistent, and provide a prototype implementation of the CrashLang compiler. We have evaluated CrashLang on five benchmarks: the Harris linked list, the Treiber stack, the Michael–Scott queue, a Read-Copy-Update binary search tree, and a Cache-Line Hash Table. We experimentally verified that each implementation correctly survives crashes.