research-article

Open access

Verifying concurrent, crash-safe systems with Perennial

Authors:

Joseph Tassarotti,

M. Frans Kaashoek,

Nickolai ZeldovichAuthors Info & Claims

SOSP '19: Proceedings of the 27th ACM Symposium on Operating Systems Principles

Pages 243 - 258

https://doi.org/10.1145/3341301.3359632

Published: 27 October 2019 Publication History

Abstract

This paper introduces Perennial, a framework for verifying concurrent, crash-safe systems. Perennial extends the Iris concurrency framework with three techniques to enable crash-safety reasoning: recovery leases, recovery helping, and versioned memory. To ease development and deployment of applications, Perennial provides Goose, a subset of Go and a translator from that subset to a model in Perennial with support for reasoning about Go threads, data structures, and file-system primitives. We implemented and verified a crash-safe, concurrent mail server using Perennial and Goose that achieves speedup on multiple cores. Both Perennial and Iris use the Coq proof assistant, and the mail server and the framework's proofs are machine checked.

References

[1]

S. Amani, J. Andronick, M. Bortin, C. Lewis, C. Rizkallah, and J. Tuong. Complx: A verification framework for concurrent imperative programs. In Proceedings of the 6th International Conference on Certified Programs and Proofs, pages 138--150, Paris, France, Jan. 2017.

Digital Library

[2]

A. Bizjak, D. Gratzer, R. Krebbers, and L. Birkedal. Iron: Managing obligations in higher-order concurrent separation logic. Proceedings of the ACM on Programming Languages, 3(POPL):65:1--65:30, Jan. 2019.

Digital Library

[3]

Q. Cao, L. Beringer, S. Gruetter, J. Dodds, and A. W. Appel. VST-Floyd: A separation logic tool to verify correctness of c programs. Journal of Automated Reasoning, 61(1-4):367--422, June 2018.

Digital Library

[4]

T. Chajed, M. F. Kaashoek, B. Lampson, and N. Zeldovich. Verifying concurrent software using movers in CSPEC. In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 307--322, Carlsbad, CA, Oct. 2018.

[5]

T. Chajed, J. Tassarotti, M. F. Kaashoek, and N. Zeldovich. Argosy: Verifying layered storage systems with recovery refinement. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 1037--1051, Phoenix, AZ, June 2019.

Digital Library

[6]

A. Charguéraud. Characteristic formulae for the verification of imperative programs. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 418--430, Tokyo, Japan, Sept. 2011.

Digital Library

[7]

H. Chen, D. Ziegler, T. Chajed, A. Chlipala, M. F. Kaashoek, and N. Zeldovich. Using Crash Hoare Logic for certifying the FSCQ file system. In Proceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP), pages 18--37, Monterey, CA, Oct. 2015.

Digital Library

[8]

A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 234--245, San Jose, CA, June 2011.

Digital Library

[9]

T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, and H. Yang. Views: Compositional reasoning for concurrent programs. In Proceedings of the 40th ACM Symposium on Principles of Programming Languages (POPL), pages 287--300, Rome, Italy, Jan. 2013.

Digital Library

[10]

G. Ernst, J. Pfähler, G. Schellhorn, and W. Reif. Modular, crash-safe refinement for ASMs with submachines. Science of Computer Programming, 131:3--21, 2016.

[11]

Google. The Go memory model, May 2014. URL https://golang.org/ref/mem.

[12]

J. Gray. Notes on data base operating systems. In R. Bayer, R. M. Graham, and G. Seegmüller, editors, Operating Systems: An Advanced Course, pages 393--481. Springer-Verlag, 1978.

[13]

R. Gu, Z. Shao, H. Chen, X. N. Wu, J. Kim, V. Sjöberg, and D. Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 653--669, Savannah, GA, Nov. 2016.

Digital Library

[14]

R. Gu, Z. Shao, J. Kim, X. Wu, J. Koenig, V. Sjöberg, H. Chen, D. Costanzo, and T. Ramananandro. Certified concurrent abstraction layers. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 646--661, Philadelphia, PA, June 2018.

Digital Library

[15]

A. Guéneau, M. O. Myreen, R. Kumar, and M. Norrish. Verified characteristic formulae for CakeML. In Proceedings of the 26th European Symposium on Programming Languages and Systems, pages 584--610, Uppsala, Sweden, Apr. 2017.

[16]

C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zill. Ironclad Apps: End-to-end security via automated full-system verification. In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 165--181, Broomfield, CO, Oct. 2014.

Digital Library

[17]

C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. Setty, and B. Zill. IronFleet: Proving practical distributed systems correct. In Proceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP), pages 1--17, Monterey, CA, Oct. 2015.

Digital Library

[18]

M. Herlihy. Wait-free synchronization. ACM Transactions on Programming Languages and Systems, 13(1):124--149, Jan. 1991.

Digital Library

[19]

M. P. Herlihy and J. M. Wing. Linearizability: a correctness condition for concurrent objects. ACM Transactions on Programming Languages Systems, 12(3):463--492, 1990.

Digital Library

[20]

R. Jung, J.-H. Jourdan, R. Krebbers, and D. Dreyer. RustBelt: Securing the foundations of the Rust programming language. Proceedings of the ACM on Programming Languages, 2(POPL):66:1--34, Dec. 2017.

Digital Library

[21]

G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, and G. Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32(1):2:1--70, Feb. 2014.

Digital Library

[22]

N. Koh, Y. Li, Y. Li, L.-y. Xia, L. Beringer, W. Honoré, W. Mansky, B. C. Pierce, and S. Zdancewic. From C to interaction trees: Specifying, verifying, and testing a networked server. In Proceedings of the 8th International Conference on Certified Programs and Proofs, pages 234--248, Cascais, Portugal, Jan. 2019.

Digital Library

[23]

B. Kragl and S. Qadeer. Layered concurrent programs. In Proceedings of the 30th International Conference on Computer Aided Verification (CAV), pages 79--102, Oxford, United Kingdom, July 2018.

[24]

R. Krebbers, R. Jung, A. Bizjak, J.-H. Jourdan, D. Dreyer, and L. Birkedal. The essence of higher-order concurrent separation logic. In Proceedings of the 26th European Symposium on Programming Languages and Systems, pages 696--723, Uppsala, Sweden, Apr. 2017.

Digital Library

[25]

M. Krogh-Jespersen, K. Svendsen, and L. Birkedal. A relational model of types-and-effects in higher-order concurrent separation logic. In Proceedings of the 44th ACM Symposium on Principles of Programming Languages (POPL), Paris, France, Jan. 2017.

Digital Library

[26]

M. Lesani, C. J. Bell, and A. Chlipala. Chapar: Certified causally consistent distributed key-value stores. In Proceedings of the 43rd ACM Symposium on Principles of Programming Languages (POPL), pages 357--370, St. Petersburg, FL, Jan. 2016.

Digital Library

[27]

P. Letouzey. Extraction in Coq: An overview. In Proceedings of the 4th Conference on Computability in Europe, pages 359--369, Athens, Greece, June 2008.

Digital Library

[28]

N. Lynch and F. Vaandrager. Forward and backward simulations - Part I: Untimed systems. Information and Computation, 121(2):214--233, Sept. 1995.

Digital Library

[29]

M. O. Myreen and S. Owens. Proof-producing synthesis of ML from higher-order logic. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 115--126, Copenhagen, Denmark, Sept. 2012.

Digital Library

[30]

L. Nelson, J. Bornholt, R. Gu, A. Baumann, E. Torlak, and X. Wang. Scaling symbolic evaluation for automated verification of systems code with Serval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP), Huntsville, Ontario, Canada, Oct. 2019.

Digital Library

[31]

G. Ntzik, P. da Rocha Pinto, and P. Gardner. Fault-tolerant resource reasoning. In Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS), pages 169--188, Pohang, South Korea, Nov.-Dec. 2015.

[32]

J. Protzenko, J.-K. Zinzindohoué, A. Rastogi, T. Ramananandro, P. Wang, S. Zanella-Béguelin, A. Delignat-Lavaud, C. Hritcu, K. Bhargavan, C. Fournet, and N. Swamy. Verified low-level programming embedded in F*. Proceedings of the ACM on Programming Languages, 1(ICFP):17:1--29, Sept. 2017.

Digital Library

[33]

I. Sergey, A. Nanevski, and A. Banerjee. Mechanized verification of fine-grained concurrent programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 77--87, Portland, OR, June 2015.

Digital Library

[34]

H. Sigurbjarnarson, J. Bornholt, E. Torlak, and X. Wang. Push-button verification of file systems via crash refinement. In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 1--16, Savannah, GA, Nov. 2016.

Digital Library

[35]

H. Sigurbjarnarson, L. Nelson, B. Castro-Karney, J. Bornholt, E. Torlak, and X. Wang. Nickel: A framework for design and verification of information flow control systems. In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 287--306, Carlsbad, CA, Oct. 2018.

[36]

A. Spector-Zabusky, J. Breitner, C. Rizkallah, and S. Weirich. Total Haskell is reasonable Coq. In Proceedings of the 7th International Conference on Certified Programs and Proofs, pages 14--27, Los Angeles, CA, Jan. 2018.

Digital Library

[37]

N. Swamy, C. Hritcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, J.-K. Zinzindohoué, and S. Zanella-Béguelin. Dependent types and multi-monadic effects in F*. In Proceedings of the 43rd ACM Symposium on Principles of Programming Languages (POPL), pages 256--270, St. Petersburg, FL, Jan. 2016.

Digital Library

[38]

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

[39]

A. Turon, D. Dreyer, and L. Birkedal. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 377--390, Boston, MA, Sept. 2013.

Digital Library

[40]

J. R. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang, M. D. Ernst, and T. Anderson. Verdi: A framework for implementing and formally verifying distributed systems. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 357--368, Portland, OR, June 2015.

Digital Library

[41]

M. Zou, H. Ding, D. Du, M. Fu, R. Gu, and H. Chen. Using concurrent relational logic with helper for verifying the AtomFS file system. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP), Huntsville, Ontario, Canada, Oct. 2019.

Digital Library

Cited By

Wang ZLan YHe XLv J(2024)A Formal Verification Approach for Linux Kernel DesigningTechnologies10.3390/technologies1208013212:8(132)Online publication date: 12-Aug-2024
https://doi.org/10.3390/technologies12080132
Lattuada AHance TBosamiya JBrun MCho CLeBlanc HSrinivasan PAchermann RChajed THawblitzel CHowell JLorch JPadon OParno BWitchel EArpaci-Dusseau ARossbach CKeeton K(2024)Verus: A Practical Foundation for Systems VerificationProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles10.1145/3694715.3695952(438-454)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1145/3694715.3695952
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
Show More Cited By

Index Terms

Verifying concurrent, crash-safe systems with Perennial
1. Software and its engineering
  1. Software organization and properties

Recommendations

Mechanized verification of fine-grained concurrent programs
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Efficient concurrent programs and data structures rarely employ coarse-grained synchronization mechanisms (i.e., locks); instead, they implement custom synchronization patterns via fine-grained primitives, such as compare-and-swap. Due to sophisticated ...
Mechanized verification of fine-grained concurrent programs
PLDI '15

Efficient concurrent programs and data structures rarely employ coarse-grained synchronization mechanisms (i.e., locks); instead, they implement custom synchronization patterns via fine-grained primitives, such as compare-and-swap. Due to sophisticated ...
Verifying read-copy-update in a logic for weak memory
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Read-Copy-Update (RCU) is a technique for letting multiple readers safely access a data structure while a writer concurrently modifies it. It is used heavily in the Linux kernel in situations where fast reads are important and writes are infrequent. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SOSP '19: Proceedings of the 27th ACM Symposium on Operating Systems Principles

October 2019

615 pages

ISBN:9781450368735

DOI:10.1145/3341301

General Chairs:
Tim Brecht
University of Waterloo
,
Carey Williamson
University of Calgary

Copyright © 2019 Owner/Author.

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

Sponsors

SIGOPS: ACM Special Interest Group on Operating Systems

In-Cooperation

USENIX Assoc: USENIX Assoc

Publisher

Association for Computing Machinery

New York, NY, United States

Publication Notes

Badge change: Article originally badged under Version 1.0 guidelines https://www.acm.org/publications/policies/artifact-review-badging

Publication History

Published: 27 October 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Conference

SOSP '19

Sponsor:

SIGOPS

SOSP '19: ACM SIGOPS 27th Symposium on Operating Systems Principles

October 27 - 30, 2019

Ontario, Huntsville, Canada

Acceptance Rates

Overall Acceptance Rate 174 of 961 submissions, 18%

Upcoming Conference

SOSP '25

Sponsor:
sigops

ACM SIGOPS 31st Symposium on Operating Systems Principles

October 13 - 16, 2025

Seoul , Republic of Korea

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

38
Total Citations
View Citations
1,482
Total Downloads

Downloads (Last 12 months)225
Downloads (Last 6 weeks)41

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang ZLan YHe XLv J(2024)A Formal Verification Approach for Linux Kernel DesigningTechnologies10.3390/technologies1208013212:8(132)Online publication date: 12-Aug-2024
https://doi.org/10.3390/technologies12080132
Lattuada AHance TBosamiya JBrun MCho CLeBlanc HSrinivasan PAchermann RChajed THawblitzel CHowell JLorch JPadon OParno BWitchel EArpaci-Dusseau ARossbach CKeeton K(2024)Verus: A Practical Foundation for Systems VerificationProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles10.1145/3694715.3695952(438-454)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1145/3694715.3695952
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
Erbsen APhilipoom JJamner DLin AGruetter SPit-Claudel CChlipala A(2024)Foundational Integration Verification of a Cryptographic ServerProceedings of the ACM on Programming Languages10.1145/36564468:PLDI(1704-1729)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656446
Spies SGäher LSammler MDreyer D(2024)Quiver: Guided Abductive Inference of Separation Logic Specifications in CoqProceedings of the ACM on Programming Languages10.1145/36564138:PLDI(889-913)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656413
Jia XYao ZPeng CZhao ZLei BLiu ELi XHe ZWang YZou XZhao CChu JWang JMiao CSekar VYu MSeneviratne AVeitch D(2024)Turbo: Efficient Communication Framework for Large-scale Data Processing ClusterProceedings of the ACM SIGCOMM 2024 Conference10.1145/3651890.3672241(540-553)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3651890.3672241
Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Asynchronous Probabilistic Couplings in Higher-Order Separation LogicProceedings of the ACM on Programming Languages10.1145/36328688:POPL(753-784)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632868
Timany AGregersen SStefanesco LHinrichsen JGondelman LNieto ABirkedal L(2024)Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional RefinementProceedings of the ACM on Programming Languages10.1145/36328518:POPL(241-272)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632851
Mansky WDu K(2024)An Iris Instance for Verifying CompCert C ProgramsProceedings of the ACM on Programming Languages10.1145/36328488:POPL(148-174)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632848
Vafeiadi Bila EDongol B(2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-1Online publication date: 31-Jul-2024
https://doi.org/10.1007/s10703-024-00462-1
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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