PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption...
summary
Claims tool-agnostic verification of crash consistency via PoWER (Preconditions on Writes Enforcing Recoverability), implements an explicit model of media corruption, and introduces a primitive called the corruption-detecting Boolean to atomically update checksums. Builds two verified systems (CapybaraKV in Verus and CapybaraNS in Dafny), CapybaraKV is ~25,000 LOC, verifies in under a minute, and reports performance competitive with unverified persistent‑memory KV stores.
AI-written summary · about
chapters (11)
- 0:00Verified persistent memory storage
- 1:43Persistent memory challenges
- 3:07Verification goals and benefits
- 4:50Crash consistency and corruption setup
- 6:53Prior verification limitations
- 9:43PoWER verification technique
- 11:50Persistent memory atomic writes
- 13:59CRC limitations in crash consistency
- 15:03Corruption Detecting Boolean primitive
- 16:04Capy Bara KV system overview
- 17:08Key contributions and lessons