Document Open Access Logo

Modular Verification of Intrusive List and Tree Data Structures in Separation Logic

Authors Marc Hermes , Robbert Krebbers

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.19.pdf
  • Filesize: 0.9 MB
  • 18 pages

Document Identifiers

Author Details

Marc Hermes
  • Radboud University, Nijmegen, The Netherlands
Robbert Krebbers
  • Radboud University, Nijmegen, The Netherlands

Acknowledgements

We thank Derek Dreyer, Laila Elbeheiry, Deepak Garg, Jules Jacobs, Ike Mulder and Michael Sammler for discussions, and the anonymous reviewers for their feedback. This research was supported in part by a generous award from Google Android Security’s ASPIRE program.

Cite AsGet BibTex

Marc Hermes and Robbert Krebbers. Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.19

Abstract

Intrusive linked data structures are commonly used in low-level programming languages such as C for efficiency and to enable a form of generic types. Notably, intrusive versions of linked lists and search trees are used in the Linux kernel and the Boost C++ library. These data structures differ from ordinary data structures in the way that nodes contain only the meta data (i.e. pointers to other nodes), but not the data itself. Instead the programmer needs to embed nodes into the data, thereby avoiding pointer indirections, and allowing data to be part of several data structures. In this paper we address the challenge of specifying and verifying intrusive data structures using separation logic. We aim for modular verification, where we first specify and verify the operations on the nodes (without the data) and then use these specifications to verify clients that attach data. We achieve this by employing a representation predicate that separates the data structure’s node structure from the data that is attached to it. We apply our methodology to singly-linked lists - from which we build cyclic and doubly-linked lists - and binary trees - from which we build binary search trees. All verifications are conducted using the Coq proof assistant, making use of the Iris framework for separation logic.

Subject Classification

ACM Subject Classification
  • Theory of computation → Separation logic
  • Theory of computation → Hoare logic
  • Theory of computation → Programming logic
  • Theory of computation → Data structures design and analysis
Keywords
  • Separation Logic
  • Program Verification
  • Data Structures
  • Iris
  • Coq

Metrics

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

Supplementary Materials

References

  1. Android Open Source Project. Buddy allocator in pKVM, 2024. URL: https://github.com/torvalds/linux/blob/master/arch/arm64/kvm/hyp/nvhe/page_alloc.c.
  2. Android Open Source Project. Source code of the hyp_pool structure used in the pKVM implementation of the buddy allocator, 2024. URL: https://github.com/torvalds/linux/blob/bf3a69c6861ff4dc7892d895c87074af7bc1c400/arch/arm64/kvm/hyp/include/nvhe/gfp.h#L12.
  3. Andrew W. Appel. Program Logics for Certified Compilers. Cambridge University Press, 2014. Google Scholar
  4. Jesper Bengtson, Jonas Braband Jensen, and Lars Birkedal. Charge! In ITP, pages 315-331, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_21.
  5. Lars Birkedal and Aleš Bizjak. Lecture notes on Iris: Higher-order concurrent separation logic, 2024. URL: https://iris-project.org/tutorial-material.html.
  6. Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. JAR, 61(1):367-422, 2018. URL: https://doi.org/10.1007/s10817-018-9457-5.
  7. Qinxiang Cao, Shengyi Wang, Aquinas Hobor, and Andrew W Appel. Proof Pearl: Magic Wand as Frame, 2018. Google Scholar
  8. Arthur Charguéraud. Higher-order representation predicates in separation logic. In CPP, pages 3-14, 2016. URL: https://doi.org/10.1145/2854065.2854068.
  9. Adam Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In PLDI, pages 234-245, 2011. URL: https://doi.org/10.1145/1993498.1993526.
  10. Marc Hermes. Coq Mechanization of "Modular Verification of Intrusive List and Tree Data Structures in Separation Logic", 2024. URL: https://doi.org/10.5281/zenodo.12575047.
  11. Gérard P. Huet. The zipper. JFP, 7(5):549-554, 1997. URL: https://doi.org/10.1017/S0956796897002864.
  12. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods, pages 41-55, 2011. URL: https://doi.org/10.1007/978-3-642-20398-5_4.
  13. Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. Higher-order ghost state. In ICFP, pages 256-269, 2016. URL: https://doi.org/10.1145/2951913.2951943.
  14. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP, 28:e20, 2018. URL: https://doi.org/10.1017/S0956796818000151.
  15. 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 POPL, pages 637-650, 2015. URL: https://doi.org/10.1145/2676726.2676980.
  16. Kernel Newbies. How does the kernel implements linked lists?, 2017. URL: https://kernelnewbies.org/FAQ/LinkedLists.
  17. Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. MoSeL: A general, extensible modal framework for interactive proofs in separation logic. PACMPL, 2(ICFP):77:1-77:30, 2018. URL: https://doi.org/10.1145/3236772.
  18. Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. The Essence of Higher-Order Concurrent Separation Logic. In ESOP, pages 696-723, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_26.
  19. Robbert Krebbers, Amin Timany, and Lars Birkedal. Interactive proofs in higher-order concurrent separation logic. In POPL, pages 205-217, 2017. URL: https://doi.org/10.1145/3009837.3009855.
  20. Olaf Krzikalla and Ion Gaztanaga. Boost.intrusive, part of Boost C++ documentation, 2024. Chapter 17, version 1.84.0. URL: https://www.boost.org/doc/libs/1_84_0/doc/html/intrusive.html.
  21. Keunhong Lee, Jeehoon Kang, Wonsup Yoon, Joongi Kim, and Sue Moon. Enveloping Implicit Assumptions of Intrusive Data Structures within Ownership Type System. In PLOS, pages 16-22, 2019. URL: https://doi.org/10.1145/3365137.3365403.
  22. Linux Kernel. Source code of red-black trees, 2021. URL: https://github.com/torvalds/linux/blob/v6.8/include/linux/rbtree_types.h#L5.
  23. Linux Kernel. Source code of linked lists library, 2023. URL: https://github.com/torvalds/linux/blob/v6.8/include/linux/list.h.
  24. Linux Kernel. Source code of container_of macro, 2023. URL: https://github.com/torvalds/linux/blob/v6.8/include/linux/container_of.h.
  25. Linux Kernel. Source code of task_struct, 2024. URL: https://github.com/torvalds/linux/blob/v6.8/include/linux/sched.h#L748.
  26. Ike Mulder, Robbert Krebbers, and Herman Geuvers. Diaframe: Automated verification of fine-grained concurrent programs in Iris. In PLDI, pages 809-824, 2022. URL: https://doi.org/10.1145/3519939.3523432.
  27. Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A Verification Infrastructure for Permission-Based Reasoning. In VMCAI, pages 41-62, 2016. URL: https://doi.org/10.1007/978-3-662-49122-5_2.
  28. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In CSL, volume 2142, pages 1-19, 2001. URL: https://doi.org/10.1007/3-540-44802-0_1.
  29. Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami. CN: Verifying Systems C Code with Separation-Logic Refinement Types. PACMPL, 7(POPL):1:1-1:32, 2023. URL: https://doi.org/10.1145/3571194.
  30. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55-74, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  31. Jan Smans, Bart Jacobs, and Frank Piessens. VeriFast for Java: A Tutorial. In Aliasing in Object-Oriented Programming. Types, Analysis and Verification, volume 7850, pages 407-442. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-36946-9_14.
  32. The Linux Kernel. What are red-black trees, and what are they for?, 2007. URL: https://docs.kernel.org/core-api/rbtree.html.
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 Imprint Privacy Contact