Towards Verifying Crash Consistency

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.