TY - GEN
T1 - Argosy
T2 - 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019
AU - Chajed, Tej
AU - Frans Kaashoek, M.
AU - Tassarotti, Joseph
AU - Zeldovich, Nickolai
N1 - Publisher Copyright:
© 2019 Copyright held by the owner/author(s).
PY - 2019/6/8
Y1 - 2019/6/8
N2 - 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 [8], 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.
AB - 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 [8], 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.
KW - Kleene Algebra
KW - Refinement
UR - http://www.scopus.com/inward/record.url?scp=85067646860&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85067646860&partnerID=8YFLogxK
U2 - 10.1145/3314221.3314585
DO - 10.1145/3314221.3314585
M3 - Conference contribution
AN - SCOPUS:85067646860
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 1054
EP - 1068
BT - PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
A2 - McKinley, Kathryn S.
A2 - Fisher, Kathleen
PB - Association for Computing Machinery
Y2 - 22 June 2019 through 26 June 2019
ER -