Document Open Access Logo

Verifying Lock-Free Search Structure Templates

Authors Nisarg Patel , Dennis Shasha , Thomas Wies

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.30.pdf
  • Filesize: 0.65 MB
  • 28 pages

Document Identifiers

Author Details

Nisarg Patel
  • New York University, NY, USA
Dennis Shasha
  • New York University, NY, USA
Thomas Wies
  • New York University, NY, USA

Funding

This work is funded in parts by NYU Wireless and by the United States National Science Foundation under grants CCF-2304758, 1840761, 2304758, and 25-74100-F1202. Further funding came from an Amazon Research Award Fall 2021. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not reflect the views of Amazon.

Acknowledgements

We thank Sebastian Wolff for many insightful discussions and his suggestions to improve the presentation of the paper.

Cite AsGet BibTex

Nisarg Patel, Dennis Shasha, and Thomas Wies. Verifying Lock-Free Search Structure Templates. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 30:1-30:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.30

Abstract

We present and verify template algorithms for lock-free concurrent search structures that cover a broad range of existing implementations based on lists and skiplists. Our linearizability proofs are fully mechanized in the concurrent separation logic Iris. The proofs are modular and cover the broader design space of the underlying algorithms by parameterizing the verification over aspects such as the low-level representation of nodes and the style of data structure maintenance. As a further technical contribution, we present a mechanization of a recently proposed method for reasoning about future-dependent linearization points using hindsight arguments. The mechanization builds on Iris' support for prophecy reasoning and user-defined ghost resources. We demonstrate that the method can help to reduce the proof effort compared to direct prophecy-based proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Separation logic
  • Theory of computation → Shared memory algorithms
Keywords
  • skiplists
  • lock-free
  • separation logic
  • linearizability
  • future-dependent linearization points
  • hindsight reasoning

Metrics

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

Related Versions

Supplementary Materials

References

  1. Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theor. Comput. Sci., 82(2):253-284, 1991. Google Scholar
  2. Parosh Aziz Abdulla, Lukás Holík, Bengt Jonsson, Ondrej Lengál, Cong Quy Trinh, and Tomás Vojnar. Verification of heap manipulating programs with ordered data by extended forest automata. In ATVA, volume 8172 of Lecture Notes in Computer Science, pages 224-239. Springer, 2013. Google Scholar
  3. Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Suha Orhun Mutluergil. Proving linearizability using forward simulations. In CAV (2), volume 10427 of Lecture Notes in Computer Science, pages 542-563. Springer, 2017. Google Scholar
  4. Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. Tada: A logic for time and data abstraction. In ECOOP, volume 8586 of Lecture Notes in Computer Science, pages 207-231. Springer, 2014. Google Scholar
  5. Brijesh Dongol and John Derrick. Verifying linearisability: A comparative survey. ACM Comput. Surv., 48(2):19:1-19:43, 2015. Google Scholar
  6. Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, and Sharon Shoham. Order out of chaos: Proving linearizability using local views. In DISC, volume 121 of LIPIcs, pages 23:1-23:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  7. Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, and Sharon Shoham. Proving highly-concurrent traversals correct. Proc. ACM Program. Lang., 4(OOPSLA):128:1-128:29, 2020. Google Scholar
  8. Mikhail Fomitchev and Eric Ruppert. Lock-free linked lists and skip lists. In PODC, pages 50-59. ACM, 2004. Google Scholar
  9. Timothy L. Harris. A pragmatic implementation of non-blocking linked-lists. In DISC, volume 2180 of Lecture Notes in Computer Science, pages 300-314. Springer, 2001. Google Scholar
  10. Maurice Herlihy and Nir Shavit. The art of multiprocessor programming. Morgan Kaufmann, 2008. Google Scholar
  11. Maurice Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, 1990. Google Scholar
  12. Prasad Jayanti, Siddhartha Jayanti, Ugur Yavuz, and Lizzie Hernandez. A universal, sound, and complete forward reasoning technique for machine-verified proofs of linearizability. PACMPL, 8(POPL), January 2024. URL: https://doi.org/10.1145/3632924.
  13. Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, and Jeehoon Kang. Modular verification of safe memory reclamation in concurrent separation logic. Proc. ACM Program. Lang., 7(OOPSLA2):828-856, 2023. Google Scholar
  14. 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. URL: https://doi.org/10.1017/S0956796818000151.
  15. Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang., 4(POPL):45:1-45:32, 2020. Google Scholar
  16. 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. ACM, 2015. Google Scholar
  17. Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew J. Parkinson. Proving linearizability using partial orders. In ESOP, volume 10201 of Lecture Notes in Computer Science, pages 639-667. Springer, 2017. Google Scholar
  18. Siddharth Krishna, Nisarg Patel, Dennis E. Shasha, and Thomas Wies. Verifying concurrent search structure templates. In PLDI, pages 181-196. ACM, 2020. Google Scholar
  19. Siddharth Krishna, Nisarg Patel, Dennis E. Shasha, and Thomas Wies. Automated Verification of Concurrent Search Structures. Synthesis Lectures on Computer Science. Morgan & Claypool Publishers, 2021. Google Scholar
  20. Siddharth Krishna, Dennis E. Shasha, and Thomas Wies. Go with the flow: compositional abstractions for concurrent data structures. Proc. ACM Program. Lang., 2(POPL):37:1-37:31, 2018. Google Scholar
  21. Siddharth Krishna, Alexander J. Summers, and Thomas Wies. Local reasoning for global graph properties. In ESOP, volume 12075 of Lecture Notes in Computer Science, pages 308-335. Springer, 2020. Google Scholar
  22. Kfir Lev-Ari, Gregory V. Chockler, and Idit Keidar. A constructive approach for proving data structures' linearizability. In DISC, volume 9363 of Lecture Notes in Computer Science, pages 356-370. Springer, 2015. Google Scholar
  23. Hongjin Liang and Xinyu Feng. Modular verification of linearizability with non-fixed linearization points. In PLDI, pages 459-470. ACM, 2013. Google Scholar
  24. Meta. Facebook Open Source Library: ConcurrentSkipList. https://github.com/facebook/folly/blob/main/folly/ConcurrentSkipList.h. Last accessed: Apr 2024.
  25. Roland Meyer, Anton Opaterny, Thomas Wies, and Sebastian Wolff. nekton: A linearizability proof checker. In CAV (1), volume 13964 of Lecture Notes in Computer Science, pages 170-183. Springer, 2023. Google Scholar
  26. Roland Meyer, Thomas Wies, and Sebastian Wolff. A concurrent program logic with a future and history. Proc. ACM Program. Lang., 6(OOPSLA2):1378-1407, 2022. Google Scholar
  27. Roland Meyer, Thomas Wies, and Sebastian Wolff. Embedding hindsight reasoning in separation logic. Proc. ACM Program. Lang., 7(PLDI):1848-1871, 2023. Google Scholar
  28. Roland Meyer, Thomas Wies, and Sebastian Wolff. Make flows small again: Revisiting the flow framework. In TACAS (1), volume 13993 of Lecture Notes in Computer Science, pages 628-646. Springer, 2023. Google Scholar
  29. Roland Meyer and Sebastian Wolff. Decoupling lock-free data structures from memory reclamation for static analysis. Proc. ACM Program. Lang., 3(POPL):58:1-58:31, 2019. Google Scholar
  30. Roland Meyer and Sebastian Wolff. Pointer life cycle types for lock-free data structures with memory reclamation. Proc. ACM Program. Lang., 4(POPL):68:1-68:36, 2020. Google Scholar
  31. Maged M. Michael. High performance dynamic lock-free hash tables and list-based sets. In SPAA, pages 73-82. ACM, 2002. Google Scholar
  32. Peter W. O'Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, and Greta Yorsh. Verifying linearizability with hindsight. In PODC, pages 85-94. ACM, 2010. Google Scholar
  33. Oracle. Java concurrent skiplist set. https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/concurrent/ConcurrentSkipListSet.html. Last accessed: Jan 2024.
  34. Nisarg Patel, Siddharth Krishna, Dennis E. Shasha, and Thomas Wies. Verifying concurrent multicopy search structures. Proc. ACM Program. Lang., 5(OOPSLA):1-32, 2021. Google Scholar
  35. Nisarg Patel, Dennis Shasha, and Thomas Wies. Verifying Lock-free Search Structure Templates / Artifact. Software (visited on 2024-08-23). URL: https://doi.org/10.4230/DARTS.10.2.15.
  36. Nisarg Patel, Dennis Shasha, and Thomas Wies. Verifying lock-free search structure templates. CoRR, abs/2405.13271, 2024. URL: https://arxiv.org/abs/2405.13271.
  37. Nisarg Patel, Dennis Shasha, and Thomas Wies. Verifying Lock-free Search Structure Templates / Artifact, April 2024. Software (visited on 2024-08-23). URL: https://doi.org/10.5281/zenodo.11051385.
  38. Alejandro Sánchez and César Sánchez. Formal verification of skiplists with arbitrary many levels. In ATVA, volume 8837 of Lecture Notes in Computer Science, pages 314-329. Springer, 2014. Google Scholar
  39. Dennis E. Shasha and Nathan Goodman. Concurrent search structure algorithms. ACM Trans. Database Syst., 13(1):53-90, 1988. Google Scholar
  40. He Zhu, Gustavo Petri, and Suresh Jagannathan. Poling: SMT aided linearizability proofs. In CAV (2), volume 9207 of Lecture Notes in Computer Science, pages 3-19. Springer, 2015. Google Scholar
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