Principles of Persistent Programming
summary
Defines a formal semantics that composes weak-memory consistency with a separate persistency order, gives both operational and declarative characterizations and proves their equivalence, and implements an execution-graph model checking tool that is an order-of-magnitude faster than naive interleaving. Builds a hardware observation setup (memory bus probe) to test Intel and ARM platforms, finds undocumented reordering on Intel despite flush/fence sequences and sporadic lost/duplicated writes on ARM, and proposes program-transform and logic techniques (volatile vs persistent variables, persistent serializability) that validate correct durable algorithms.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:28Speaker overview
- 4:19What is persistent programming
- 10:03Programming language models
- 16:27Weak memory concurrency
- 23:56Non-volatile memory emergence
- 26:43Semantics of persistent apps
- 35:01Weak memory and persistency
- 36:24Litmus tests for hardware
- 41:01Correctness for persistent algorithms
- 43:54Persistent linearizability
- 44:17Program logics for persistence
- 46:26Model checking persistent systems
- 53:13Future of non-volatile memory
- 55:07Q&A
related talks
15mTowards a Formal Foundation of Intermittent Computing
57mInvited Talk: Bridging Safety and Performance
15mTowards Verifying Crash Consistency
25mResponsive Parallelism with Synchronization
18mCompiler-Assisted Crash Consistency for PMEM
19mPete's Footprints
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
22mA Formal Model for Portable, Heterogeneous Accelerator Programming