Argosy: verifying layered storage systems with recovery refinement
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich · 2019
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.