Verifying Concurrent, Crash-Safe Systems with Perennial
summary
Perennial is a mechanized extension of Iris that proves crash safety for concurrent programs and imports Go via goose to verify real code; it verifies the GoTxn concurrent transaction layer and underpins a mountable Daisy NFS server. Key claims: per-thread crash conditions plus a post-crash modality let recovery be proven idempotent, recovery correctness composes with thread-local reasoning, and the project accumulates about 30,000 lines of proof while yielding performance comparable to Linux NFS.
AI-written summary · about
chapters (17)
- 0:00Start
- 2:02A Simple Disk Replication Library
- 2:35Thread Safety
- 3:55How Does Recovery Work
- 9:12Separating Conjunction
- 10:01Concurrent Composition Rule
- 13:26Crash Condition
- 17:56Crashes Modify State
- 21:25Replicated Disk Recovery
- 24:29Ownership Transfer
- 30:01Famous Framing Principle
- 30:24Frame Rule
- 33:31Linearizability and Atomicity
- 44:32Benchmarks
- 45:36Scalability for Multi-Threaded Execution
- 46:27Fault-Tolerant Csl
- 49:26Synchronous Disk Model
related talks
42mJepsen 9: A Fsyncing Feeling
20mPerformal: Formal Verification of Latency Properties for Distributed Systems
44mThe Simplest Way to Build Resilient Applications
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
57mReliability Nirvana
55mGoing Resilient
48mThe Verification of a Distributed System
20mAn Automated Scalable RISC-V Cache Coherency Verification Project