Document Open Access Logo

Modular Verification of State-Based CRDTs in Separation Logic

Authors Abel Nieto , Arnaud Daby-Seesaram , Léon Gondelman , Amin Timany , Lars Birkedal

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.22.pdf
  • Filesize: 1.05 MB
  • 27 pages

Document Identifiers

Author Details

Abel Nieto
  • Aarhus University, Denmark
Arnaud Daby-Seesaram
  • ENS Paris-Saclay, France
Léon Gondelman
  • Aarhus University, Denmark
Amin Timany
  • Aarhus University, Denmark
Lars Birkedal
  • Aarhus University, Denmark

Funding

This work was supported in part by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation.

Cite As Get BibTex

Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal. Modular Verification of State-Based CRDTs in Separation Logic. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 22:1-22:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ECOOP.2023.22

Abstract

Conflict-free Replicated Datatypes (CRDTs) are a class of distributed data structures that are highly-available and weakly consistent. The CRDT taxonomy is further divided into two subclasses: state-based and operation-based (op-based). Recent prior work showed how to use separation logic to verify convergence and functional correctness of op-based CRDTs while (a) verifying implementations (as opposed to high-level protocols), (b) giving high level specifications that abstract from low-level implementation details, and (c) providing specifications that are modular (i.e. allow client code to use the CRDT like an abstract data type). We extend this separation logic approach to verification of CRDTs to handle state-based CRDTs, while respecting the desiderata (a)-(c). The key idea is to track the state of a CRDT as a function of the set of operations that produced that state. Using the observation that state-based CRDTs are automatically causally-consistent, we obtain CRDT specifications that are agnostic to whether a CRDT is state- or op-based. When taken together with prior work, our technique thus provides a unified approach to specification and verification of op- and state-based CRDTs. We have tested our approach by verifying StateLib, a library for building state-based CRDTs. Using StateLib, we have further verified convergence and functional correctness of multiple example CRDTs from the literature. Our proofs are written in the Aneris distributed separation logic and are mechanized in Coq.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Distributed algorithms
  • Theory of computation → Separation logic
Keywords
  • separation logic
  • distributed systems
  • CRDT
  • replicated data type
  • formal verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Lars Birkedal and Aleš Bizjak. Lecture notes on iris: Higher-order concurrent separation log, 2017. URL: http://iris-project.org/tutorial-pdfs/iris-lecture-notes.pdf.
  2. Kenneth Birman, Andre Schiper, and Pat Stephenson. Lightweight causal and atomic group multicast. ACM Transactions on Computer Systems (TOCS), 9(3):272-314, 1991. URL: https://doi.org/10.1145/128738.128742.
  3. Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. Replicated data types: Specification, verification, optimality. In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pages 271-284. ACM, January 2014. URL: https://doi.org/10.1145/2535838.2535848.
  4. Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, and Derek Dreyer. Compass: strong and compositional library specifications in relaxed memory separation logic. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 792-808, 2022. Google Scholar
  5. Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Concurrent data structures linked in time. arXiv preprint, 2016. URL: https://arxiv.org/abs/1604.08080.
  6. Stephen Dolan, K. C. Sivaramakrishnan, and Anil Madhavapeddy. Bounding data races in space and time. In PLDI, pages 242-255. ACM, 2018. Google Scholar
  7. Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. Verifying strong eventual consistency in distributed systems. Proc. ACM Program. Lang., 1(OOPSLA):109:1-109:28, 2017. URL: https://doi.org/10.1145/3133933.
  8. Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal. Distributed causal memory: Modular specification and verification in higher-order distributed separation logic. Proc. ACM Program. Lang., 5(POPL):1-29, 2021. URL: https://doi.org/10.1145/3434323.
  9. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28:e20, 2018. Google Scholar
  10. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 637-650. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676980.
  11. Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, and Lars Birkedal. Aneris: A mechanised logic for modular reasoning about distributed systems. In ESOP, volume 12075 of Lecture Notes in Computer Science, pages 336-365. Springer, 2020. Google Scholar
  12. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558-565, 1978. URL: https://doi.org/10.1145/359545.359563.
  13. Adriaan Leijnse, Paulo Sérgio Almeida, and Carlos Baquero. Higher-order patterns in replicated data types. In PaPoC@EuroSys, pages 5:1-5:6. ACM, 2019. URL: https://doi.org/10.1145/3301419.3323971.
  14. Hongjin Liang and Xinyu Feng. Abstraction for conflict-free replicated data types. In Stephen N. Freund and Eran Yahav, editors, PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 20211, pages 636-650. ACM, 2021. URL: https://doi.org/10.1145/3453483.3454067.
  15. Barbara H. Liskov and Stephen N. Zilles. Programming with abstract data types. In SIGPLAN Symposium on Very High Level Languages, pages 50-59. ACM, 1974. Google Scholar
  16. Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, and Niki Vazou. Verifying replicated data types with typeclass refinements in liquid haskell. Proc. ACM Program. Lang., 4(OOPSLA):216:1-216:30, 2020. URL: https://doi.org/10.1145/3428284.
  17. Kartik Nagar and Suresh Jagannathan. Automated parameterized verification of crdts. In CAV (2), volume 11562 of Lecture Notes in Computer Science, pages 459-477. Springer, 2019. Google Scholar
  18. Sreeja S. Nair, Gustavo Petri, and Marc Shapiro. Proving the safety of highly-available distributed objects. In ESOP, volume 12075 of Lecture Notes in Computer Science, pages 544-571. Springer, 2020. Google Scholar
  19. Aleksandar Nanevski. Separation logic and concurrency. oregon programming languages summer school, 2016. Google Scholar
  20. Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, and Lars Birkedal. Modular verification of op-based crdts in separation logic. Proc. ACM Program. Lang. OOPSLA (2022). Accepted for publication, 2022. Google Scholar
  21. Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. A comprehensive study of convergent and commutative replicated data types. Research Report 7506, INRIA, January 2011. URL: http://hal.inria.fr/inria-00555588/.
  22. Amin Timany and Lars Birkedal. Reasoning about monotonicity in separation logic. In CPP, pages 91-104. ACM, 2021. Google Scholar
  23. Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Léon Gondelman, Abel Nieto, and Lars Birkedal. Trillium: Unifying refinement and higher-order distributed separation logic. CoRR, abs/2109.07863, 2021. Google Scholar
  24. Peter Zeller, Annette Bieniusa, and Arnd Poetzsch-Heffter. Formal specification and verification of crdts. In FORTE, volume 8461 of Lecture Notes in Computer Science, pages 33-48. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43613-4_3.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact