Argosy: Verifying Layered Storage Systems With Recovery Refinement

Опубликовано 31 июля 2019, 1:53

Storage systems make persistence guarantees even if the system crashes at any time, which they achieve using recovery procedures that run after a crash. Realistic storage systems are built using layered abstractions, built on top of one another. In this talk, I’ll present Argosy, a framework for machine-checked proofs of storage systems that supports reasoning about multiple layers with modular proofs. Reasoning about layered storage systems, in particular, is especially challenging due to recovery: the system can crash in the middle of a high-level recovery procedure and must start over with the lowest-level recovery procedure.

This work introduces recovery refinement, a set of conditions that ensure proper implementation of an interface with a recovery procedure. Argosy includes a proof that recovery refinements compose, using Kleene algebra for concise definitions and metatheory. We implemented Crash Hoare Logic, the program logic used by FSCQ, to prove recovery refinement, and demonstrated the whole system by verifying an example of layered recovery featuring a write-ahead log running on top of a disk replication system. The metatheory of the framework, the soundness of the program logic, and these examples are all verified in the Coq proof assistant.

Slides and more at microsoft.com/en-us/research/v...