Coursera Spring Sale
40% Off Coursera Plus Annual!
Grab it
Explore a 15-minute conference presentation from OOPSLA 2025 that introduces CrashLang, a novel programming language and type system designed to guarantee crash consistency in persistent memory applications. Learn how researchers from UC Irvine address the critical challenge of ensuring data remains consistent after system crashes in technologies like Compute Express Link (CXL) memory sharing and persistent memory. Discover the commit-store pattern implementation that enables a single store operation to logically commit entire data structure operations, providing formal guarantees that well-typed programs maintain crash consistency. Examine the theoretical foundations through formal proofs and explore practical applications demonstrated on five benchmark implementations including the Harris linked list, Treiber stack, Michael-Scott queue, Read-Copy-Update binary search tree, and Cache-Line Hash Table. Gain insights into how this approach moves beyond existing bug-finding tools to provide actual verification guarantees for crash-consistent programming, with access to reusable artifacts and supplementary materials for further exploration.
