Argosy: verifying layered storage systems with recovery refinement
Argosy: verifying layered storage systems with recovery refinement
复制标题
DOI：
10.1145/3314221.3314585
复制
发表时间：
2019-06
期刊：
影响因子：
--
通讯作者：
Tej Chajed;Joseph Tassarotti;M. Kaashoek;Nickolai Zeldovich
中科院分区：
文献类型：
--
作者：
Tej Chajed;Joseph Tassarotti;M. Kaashoek;Nickolai Zeldovich
存储系统即使系统在崩溃后运行的恢复过程中的任何时间都可以保证，我们提出了一个机器检查的框架关于分层的恢复过程尤其具有挑战性，因为系统可以在更抽象的层恢复过程的中间崩溃，并且必须从最低级别的恢复过程开始。使用恢复过程的接口包括一个证明恢复改进，使用Kleene代数进行简洁的定义和Metatheory。在磁盘复制系统上运行的层次恢复的示例。
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.