research-article

Open access

Argosy: verifying layered storage systems with recovery refinement

Authors:

Joseph Tassarotti,

M. Frans Kaashoek,

Nickolai ZeldovichAuthors Info & Claims

PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 1054 - 1068

https://doi.org/10.1145/3314221.3314585

Published: 08 June 2019 Publication History

Abstract

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.

Supplementary Material

WEBM File (p1054-chajed.webm)

Download
73.36 MB

MP4 File (3314221.3314585.mp4)

Video Presentation

Download
48.74 MB

References

[1]

Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: semantic foundations for networks. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014. 113–126.

Digital Library

[2]

Robert Atkey. 2009. Parameterised notions of computation. J. Funct. Program. 19, 3-4 (2009), 335–376.

Digital Library

[3]

Ryan Beckett, Eric Campbell, and Michael Greenberg. 2017. Kleene Algebra Modulo Theories. arXiv: cs.PL/1707.02894

[4]

Ryan Beckett, Michael Greenberg, and David Walker. 2016. Temporal NetKAT. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016. 386–401.

Digital Library

[5]

Thomas Braibant and Damien Pous. 2012. Deciding Kleene Algebras in Coq. Logical Methods in Computer Science 8, 1 (2012).

[6]

Haogang Chen. 2016. Certifying a Crash-safe File System. Ph.D. Dissertation. Massachusetts Institute of Technology.

[7]

Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay İleri, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2017. Verifying a high-performance crash-safe file system using a tree specification. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP). Shanghai, China, 270–286.

Digital Library

[8]

Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2015. Using Crash Hoare Logic for Certifying the FSCQ File System. In Proceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP). Monterey, CA, 18–37.

Digital Library

[9]

Ernie Cohen. 1994. Lazy Caching in Kleene Algebra.

[10]

Gidon Ernst. 2016. A Verified POSIX-Compliant Flash File System -Modular Verification Technology & Crash Tolerance. Ph.D. Dissertation. Augsburg University.

[11]

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, and Wolfgang Reif. 2016. Modular, crash-safe refinement for ASMs with submachines. Science of Computer Programming 131 (2016), 3–21.

[12]

Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic NetKAT. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 282–309.

[13]

Sergey Goncharov, Lutz Schröder, and Till Mossakowski. 2009. Kleene Monads: Handling Iteration in a Framework of Generic Effects. In Proceedings of the 3rd International Conference on Algebra and Coalgebra in Computer Science (CALCO’09). Springer-Verlag, Berlin, Heidelberg, 18–33. http://dl.acm.org/citation.cfm?id=1812941.1812945

Digital Library

[14]

Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. 2018. Certified Concurrent Abstraction Layers. In Proceedings of the 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Philadelphia, PA.

Digital Library

[15]

Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. 2015. IronFleet: Proving Practical Distributed Systems Correct. In Proceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP). Monterey, CA, 1–17.

Digital Library

[16]

Jan Kara. 2012. jbd2: issue cache flush after checkpointing even with internal journal. http://git.kernel.org/ cgit/linux/kernel/git/stable/linux-stable.git/commit/?id= 79feb521a44705262d15cc819a4117a447b11ea7 .

[17]

Jan Kara. 2014. {PATCH} ext4: Forbid journal_async_commit in data=ordered mode. http://permalink.gmane.org/gmane.comp. file-systems.ext4/46977 .

[18]

Dexter Kozen. 1990. On Kleene Algebras and Closed Semirings. In MFCS (Lecture Notes in Computer Science), Vol. 452. Springer, 26–47.

Digital Library

[19]

Dexter Kozen. 1998. Typed Kleene algebra. Technical Report TR98-1669. Computer Science Department, Cornell University.

[20]

Dexter Kozen and Maria-Christina Patron. 2000. Certification of Compiler Optimizations Using Kleene Algebra with Tests. In Computational Logic - CL 2000, First International Conference, London, UK, 24-28 July, 2000, Proceedings. 568–582.

Digital Library

[21]

Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley.

Digital Library

[22]

Hongjin Liang, Xinyu Feng, and Ming Fu. 2012. A Rely-guaranteebased Simulation for Verifying Concurrent Program Transformations. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’12). ACM, New York, NY, USA, 455–468.

Digital Library

[23]

Lanyue Lu, Andrea C. Arpaci-Dusseau, Remzi H. Arpaci-Dusseau, and Shan Lu. 2013. A Study of Linux File System Evolution. In Proceedings of the 11th USENIX Conference on File and Storage Technologies (FAST). San Jose, CA, 31–44.

Digital Library

[24]

Nancy Lynch and Frits Vaandrager. 1995. Forward and Backward Simulations – Part I: Untimed Systems. Information and Computation 121, 2 (Sept. 1995), 214–233.

Digital Library

[25]

Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann.

Digital Library

[26]

Gian Ntzik, Pedro da Rocha Pinto, and Philippa Gardner. 2015. Faulttolerant Resource Reasoning. In Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS). Pohang, South Korea.

[27]

Damien Pous. 2013. Kleene Algebra with Tests and Coq Tools for while Programs. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. 180–196.

Digital Library

[28]

Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Push-Button Verification of File Systems via Crash Refinement. In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI). Savannah, GA.

Digital Library

[29]

The Coq Development Team. 2019. The Coq Proof Assistant, version 8.9.0.

[30]

J. von Wright. 2004. Towards a refinement algebra. Science of Computer Programming 51, 1 (2004), 23 – 45.

Digital Library

[31]

James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. 2015. Verdi: A Framework for Implementing and Formally Verifying Distributed Systems. In Proceedings of the 2015 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Portland, OR, 357–368.

Digital Library

Cited By

Oliveira Vale AWang ZChen YYou PShao Z(2024)Compositionality and Observational Refinement for Linearizability with CrashesProceedings of the ACM on Programming Languages10.1145/36897928:OOPSLA2(2296-2324)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689792
Kappé TSchmid TSilva A(2023)A Complete Inference System for Skip-free Guarded Kleene Algebra with TestsProgramming Languages and Systems10.1007/978-3-031-30044-8_12(309-336)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_12
Chang YHsiao YLin TTsao CWu CChang YKo HChen YLu SHowell J(2020)Determinizing crash behavior with a verified snapshot-consistent flash translation layerProceedings of the 14th USENIX Conference on Operating Systems Design and Implementation10.5555/3488766.3488771(81-97)Online publication date: 4-Nov-2020
https://dl.acm.org/doi/10.5555/3488766.3488771
Show More Cited By

Index Terms

Argosy: verifying layered storage systems with recovery refinement
1. Hardware
  1. Robustness
    1. Fault tolerance
      1. System-level fault tolerance
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Substructural logic and partial correctness

We formulate a noncommutative sequent calculus for partial correctness that subsumes propositional Hoare Logic. Partial correctness assertions are represented by intuitionistic linear implication. We prove soundness and completeness over relational and ...
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
Automated Reasoning with Analytic Tableaux and Related Methods
Abstract
We employ a recently developed methodology—called structural refinement—to extract nested sequent systems for a sizable class of intuitionistic modal logics from their respective labelled sequent systems. This method can be seen as a means by ...
On Hoare logic and Kleene algebra with tests

We show that Kleene algebra with tests (KAT) subsumes propositional Hoare logic (PHL). Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by simple equational reasoning. In addition, we show that all ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2019

1162 pages

ISBN:9781450367127

DOI:10.1145/3314221

General Chair:
Kathryn S. McKinley
Google, USA
,
Program Chair:
Kathleen Fisher
Tufts University, USA

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 June 2019

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

PLDI '19

Sponsor:

SIGPLAN

PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 22 - 26, 2019

AZ, Phoenix, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
509
Total Downloads

Downloads (Last 12 months)95
Downloads (Last 6 weeks)25

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Oliveira Vale AWang ZChen YYou PShao Z(2024)Compositionality and Observational Refinement for Linearizability with CrashesProceedings of the ACM on Programming Languages10.1145/36897928:OOPSLA2(2296-2324)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689792
Kappé TSchmid TSilva A(2023)A Complete Inference System for Skip-free Guarded Kleene Algebra with TestsProgramming Languages and Systems10.1007/978-3-031-30044-8_12(309-336)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_12
Chang YHsiao YLin TTsao CWu CChang YKo HChen YLu SHowell J(2020)Determinizing crash behavior with a verified snapshot-consistent flash translation layerProceedings of the 14th USENIX Conference on Operating Systems Design and Implementation10.5555/3488766.3488771(81-97)Online publication date: 4-Nov-2020
https://dl.acm.org/doi/10.5555/3488766.3488771
Mehta MCook W(2020)Separation Logic-Based Verification Atop a Binary-Compatible Filesystem ModelFormal Methods: Foundations and Applications10.1007/978-3-030-63882-5_10(155-170)Online publication date: 25-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-63882-5_10
Chajed TTassarotti JKaashoek MZeldovich NBrecht TWilliamson C(2019)Verifying concurrent, crash-safe systems with PerennialProceedings of the 27th ACM Symposium on Operating Systems Principles10.1145/3341301.3359632(243-258)Online publication date: 27-Oct-2019
https://dl.acm.org/doi/10.1145/3341301.3359632

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents