Towards Verifying Crash Consistency
summary
Guarantees crash consistency for well-typed implementations by proving a type system and compiling to Rust that inserts fences/flushes; the paper ships a prototype compiler and reusable artifacts and verifies five lock-free structures (Harris list, Treiber stack, Michael–Scott queue, RCU BST, cache-line hash table) under millions of injected partial crashes with no violations. Core ideas are CrashLang type system tracking pristine references, enforcing the commit-store pattern, and a backend that auto-inserts persistence operations.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:22Persistent memory and CXL
- 1:45All-or-nothing semantics
- 3:29CrashLang workflow
- 4:11Harris lock-free list
- 6:37Deletion in data structures
- 8:45Type system features
- 10:10CrashLang evaluation
- 11:58Summary
- 12:20Q&A
related talks
20mScalable and Accurate Application-Level Crash-Consistency Testing(…)
13mA Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
47mHow to trust a verified program?
31mModel Checking Distributed Software Systems
01h 03mPrinciples of Persistent Programming
25mContinuous compliance with Rust in automotive software
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
01h 08mFireside chat