Article

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems

Authors:

Morten Krogh-Jespersen,

Marit Edna Ohlenbusch,

Simon Oddershede Gregersen,

Lars BirkedalAuthors Info & Claims

Programming Languages and Systems: 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings

Pages 336 - 365

https://doi.org/10.1007/978-3-030-44914-8_13

Published: 27 April 2020 Publication History

Abstract

Building network-connected programs and distributed systems is a powerful way to provide scalability and availability in a digital, always-connected era. However, with great power comes great complexity. Reasoning about distributed systems is well-known to be difficult. In this paper we present Aneris, a novel framework based on separation logic supporting modular, node-local reasoning about concurrent and distributed systems. The logic is higher-order, concurrent, with higher-order store and network sockets, and is fully mechanized in the Coq proof assistant. We use our framework to verify an implementation of a load balancer that uses multi-threading to distribute load amongst multiple servers and an implementation of the two-phase-commit protocol with a replicated logging service as a client. The two examples certify that Aneris is well-suited for both horizontal and vertical modular reasoning.

References

[1]

Birkedal, L., Bizjak, A.: Lecture notes on Iris: Higher-order concurrent separation logic (2017), URL http://iris-project.org/tutorial-pdfs/iris-lecture-notes.pdf

[2]

Deniélou, P., Yoshida, N.: Dynamic multirole session types. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26–28, 2011, pp. 435–446, ACM (2011),

[3]

Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23–25, 2013, pp. 287–300, ACM (2013),

[4]

Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D’Hondt, T. (ed.) ECOOP 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21–25, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6183, pp. 504–528, Springer (2010),

[5]

Floyd, R.W.: Assigning meanings to programs. Mathematical aspects of computer science 19(19–32), 1 (1967)

[6]

Gray, J.: Notes on data base operating systems. In: Flynn, M.J., Gray, J., Jones, A.K., Lagally, K., Opderbeck, H., Popek, G.J., Randell, B., Saltzer, J.H., Wiehle, H. (eds.) Operating Systems, An Advanced Course, Lecture Notes in Computer Science, vol. 60, pp. 393–481, Springer (1978),

[7]

Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving practical distributed systems correct. In: Miller, E.L., Hand, S. (eds.) Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4–7, 2015, pp. 1–17, ACM (2015),

[8]

Hinrichsen, J.K., Bengtson, J., Krebbers, R.: Actris: session-type based reasoning in separation logic. PACMPL 4, 6:1–6:30 (2020),

[9]

Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997),

[10]

Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C.(ed.) Programming Languages and Systems - ESOP’98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, Lecture Notes in Computer Science, vol. 1381, pp. 122–138. Springer (1998),

[11]

Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7–12, 2008, pp. 273–284, ACM (2008),

[12]

Jung, R., Jourdan, J., Krebbers, R., Dreyer, D.: Rustbelt: securing the foundations of the rust programming language. PACMPL 2(POPL), 66:1–66:34 (2018),

[13]

Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, p. 256–269, ICFP 2016, Association for Computing Machinery, New York, NY, USA (2016), ISBN 9781450342193,

[14]

Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018),

[15]

Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15–17, 2015, pp. 637–650, ACM (2015),

[16]

Kaiser, J., Dang, H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In: Müller, P. (ed.) 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19–23, 2017, Barcelona, Spain, LIPIcs, vol. 74, pp. 17:1–17:29, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017),

[17]

Killian, C.E., Anderson, J.W., Braud, R., Jhala, R., Vahdat, A.: Mace: language support for building distributed systems. In: Ferrante, J., McKinley, K.S. (eds.) Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10–13, 2007, pp. 179–188, ACM (2007),

[18]

Krebbers, R., Jung, R., Bizjak, A., Jourdan, J., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: Yang, H. (ed.) Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10201, pp. 696–723, Springer (2017),

[19]

Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18–20, 2017, pp. 205–217, ACM (2017)

[20]

Krogh-Jespersen, M., Timany, A., Ohlenbusch, M.E., Gregersen, S.O., Birkedal, L.: Aneris: A mechanised logic for modular reasoning about distributed systems - technical appendix (2020), URL https://iris-project.org/pdfs/2020-esop-aneris-final-appendix.pdf

[21]

Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2), 125–143 (1977),

[22]

Lamport, L.: The implementation of reliable distributed multiprocess systems. Computer Networks 2, 95–114 (1978),

[23]

Lamport, L.: Hybrid systems in TLA

^{+}

. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems, Lecture Notes in Computer Science, vol. 736, pp. 77–102, Springer (1992),

[24]

Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6355, pp. 348–370, Springer (2010),

[25]

Lesani, M., Bell, C.J., Chlipala, A.: Chapar: certified causally consistent distributed key-value stores. In: Bodík, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20–22, 2016, pp. 357–370, ACM (2016),

[26]

Ley-Wild, R., Nanevski, A.: Subjective auxiliary state for coarse-grained concurrency. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23–25, 2013, pp. 561–574, ACM (2013),

[27]

Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.A.: Communicating state transition systems for fine-grained concurrent resources. In: Shao, Z. (ed.) Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014, Proceedings, Lecture Notes in Computer Science, vol. 8410, pp. 290–310, Springer (2014),

[28]

O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007),

[29]

Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pp. 46–57, IEEE Computer Society (1977),

[30]

Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: Formal specification, verification, and implementation of fault-tolerant systems using EventML. ECEASST 72 (2015),

[31]

Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems. Sci. Comput. Program. 148, 26–48 (2017),

[32]

Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22–25 July 2002, Copenhagen, Denmark, Proceedings, pp. 55–74, IEEE Computer Society (2002),

[33]

da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: Tada: A logic for time and data abstraction. In: Jones, R.E. (ed.) ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, July 28 - August 1, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8586, pp. 207–231, Springer (2014),

[34]

Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: Grove, D., Blackburn, S. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15–17, 2015, pp. 77–87, ACM (2015),

[35]

Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. PACMPL 2(POPL), 28:1–28:30 (2018),

[36]

Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014, Proceedings, Lecture Notes in Computer Science, vol. 8410, pp. 149–168, Springer (2014),

[37]

Timany, A., Stefanesco, L., Krogh-Jespersen, M., Birkedal, L.: A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. PACMPL 2(POPL), 64:1–64:28 (2018),

[38]

Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: Schneider-Kamp, P., Hanus, M. (eds.) Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 20–22, 2011, Odense, Denmark, pp. 161–172, ACM (2011),

[39]

Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: Morrisett, G., Uustalu, T. (eds.) ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25–27, 2013, pp. 377–390, ACM (2013),

[40]

Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.E.: Verdi: a framework for implementing and formally verifying distributed systems. In: Grove, D., Blackburn, S. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15–17, 2015, pp. 357–368, ACM (2015),

Cited By

Somers TKrebbers R(2024)Verified Lock-Free Session Channels with LinkingProceedings of the ACM on Programming Languages10.1145/36897328:OOPSLA2(588-617)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689732
Qiu LKim YShin JKim JHonoré WShao Z(2024)LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness ProofsProceedings of the ACM on Programming Languages10.1145/36564238:PLDI(1140-1164)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656423
Castello JRedmond PKuper L(2024)Inductive Diagrams for Causal ReasoningProceedings of the ACM on Programming Languages10.1145/36498308:OOPSLA1(529-554)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649830
Show More Cited By

Index Terms

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems

Index terms have been assigned to the content through auto-classification.

Recommendations

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement

Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features and to support modular reasoning about imperative higher-order concurrent and distributed programs. Step- indexing comes, however, with an inherent ...
Distributed causal memory: modular specification and verification in higher-order distributed separation logic

We present the first specification and verification of an implementation of a causally-consistent distributed database that supports modular verification of full functional correctness properties of clients and servers. We specify and reason about the ...
Mechanised Assessment of Complex Natural-Language Arguments Using Expressive Logic Combinations
Frontiers of Combining Systems
Abstract
We present and illustrate an approach to combining logics based on shallow semantical embeddings, a technique that harnesses the high expressive power of classical higher-order logic (HOL) as a meta-language in order to embed the syntax and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Programming Languages and Systems: 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings

Apr 2020

784 pages

ISBN:978-3-030-44913-1

DOI:10.1007/978-3-030-44914-8

Editor:
Peter Müller
ETH Zurich, Zurich, Switzerland

© The Author(s) 2020.

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 April 2020

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Somers TKrebbers R(2024)Verified Lock-Free Session Channels with LinkingProceedings of the ACM on Programming Languages10.1145/36897328:OOPSLA2(588-617)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689732
Qiu LKim YShin JKim JHonoré WShao Z(2024)LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness ProofsProceedings of the ACM on Programming Languages10.1145/36564238:PLDI(1140-1164)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656423
Castello JRedmond PKuper L(2024)Inductive Diagrams for Causal ReasoningProceedings of the ACM on Programming Languages10.1145/36498308:OOPSLA1(529-554)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649830
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
Nagasamudram RBeringer LBirman KMilano MNaumann D(2024)Verifying a C Implementation of Derecho’s Coordination Mechanism Using VST and CoqNASA Formal Methods10.1007/978-3-031-60698-4_6(99-117)Online publication date: 4-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-60698-4_6
Gondelman LHinrichsen JPereira MTimany ABirkedal L(2023)Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation ProtocolsProceedings of the ACM on Programming Languages10.1145/36078597:ICFP(847-877)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3607859
Wagner CJaber NSamanta R(2023)Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded RegionsProceedings of the ACM on Programming Languages10.1145/35860337:OOPSLA1(172-200)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586033
Redmond PShen GVazou NKuper L(2022)Verified Causal Broadcast with Liquid HaskellProceedings of the 34th Symposium on Implementation and Application of Functional Languages10.1145/3587216.3587222(1-13)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3587216.3587222
Nieto AGondelman LReynaud ATimany ABirkedal L(2022)Modular verification of op-based CRDTs in separation logicProceedings of the ACM on Programming Languages10.1145/35633516:OOPSLA2(1788-1816)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563351
Spies SGäher LTassarotti JJung RKrebbers RBirkedal LDreyer D(2022)Later credits: resourceful reasoning for the later modalityProceedings of the ACM on Programming Languages10.1145/35476316:ICFP(283-311)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547631
Show More Cited By

View Options

View options

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