Argosy: Verifying Layered Storage Systems with Recovery Refinement
Storage systems make persistence guarantees even if the system crashes at any time, which they achieve using recovery procedures that run after a crash. We present Argosy, a framework for machine-checked proofs of storage systems that supports layered recovery implementations with modular proofs. Reasoning about layered recovery procedures is especially challenging because the system can crash in the middle of a more abstract layer’s recovery procedure and must start over with the lowest-level recovery procedure.
This paper 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.
Wed 26 Jun Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change
|08:30 - 08:50|
Berkeley ChurchillStanford University, Oded PadonStanford University, Rahul SharmaMicrosoft Research, Alex AikenStanford UniversityMedia Attached
|08:50 - 09:10|
Andreas LööwChalmers University of Technology, Ramana KumarDeepMind, Yong Kiam TanCarnegie Mellon University, USA, Magnus O. MyreenChalmers University of Technology, Sweden, Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, Oskar AbrahamssonChalmers University of Technology, Sweden, Anthony FoxUniversity of Cambridge, UKDOI Pre-print Media Attached
|09:10 - 09:30|
Tej ChajedMassachusetts Institute of Technology, USA, Joseph TassarottiBoston College, M. Frans KaashoekMassachusetts Institute of Technology, USA, Nickolai ZeldovichMassachusetts Institute of Technology, USADOI Pre-print Media Attached