Document Open Access Logo

Verifying Wait-Freedom for Concurrent Higher-Order Programs

Authors Egor Namakonov , Lars Birkedal , Amin Timany

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2026.20.pdf
  • Filesize: 1.47 MB
  • 29 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Theory of computation → Logic and verification
  • Theory of computation → Concurrency
Keywords
  • separation logic
  • higher-order logic
  • concurrency
  • formal verification

Metrics

Abstract

Wait-freedom is the strongest non-blocking progress guarantee for concurrent data structures, ensuring that every operation completes in a finite number of steps regardless of interference from other threads. While verification of wait-freedom has been studied for first-order languages, verifying it for higher-order programming languages with general references remains an open challenge. In such languages, operations may be used by arbitrary, unverified higher-order clients, making it unclear how to even define wait-freedom formally in terms of programs' semantics, let alone prove it.
In this paper, we present the first framework for verifying wait-freedom of concurrent programs written in a higher-order language with general references. Our approach is based on the Lawyer concurrent separation logic which has been recently introduced for termination verification. We identify a specification pattern in the Lawyer logic that captures wait-freedom. To establish this connection formally, we prove a novel adequacy theorem for Lawyer which states that programs which are proven correct in the Lawyer logic against a specification in the aforementioned specification pattern are wait-free. Proving wait-freedom requires to show that all calls made to operations by any arbitrary client terminate. Thus, as a part of proving the adequacy theorem above, we need to prove that the behavior of the client of the data structure is safe in the sense that it does not break the internal invariants of the data structure, e.g., by directly manipulating the data structure’s internal state. To this end, we develop a logical relations model that establishes safety for all clients once and for all.
We demonstrate the effectiveness of our approach by proving wait-freedom for several representative examples, including a higher-order list map function, and a memory-efficient single-producer, single-consumer queue. For the latter, wait-freedom is conditional in that, as the name suggests, there can be at most one enqueuer thread and one dequeuer thread. To capture this formally, we introduce the notion of restricted wait-freedom as a variant of wait-freedom that restricts the number of concurrent threads, and show how our approach can support reasoning about restricted wait-freedom. All our results have been mechanized on top of the Rocq Prover and using the Iris separation logic framework that Lawyer is also based on.

Cite As Get BibTex

Egor Namakonov, Lars Birkedal, and Amin Timany. Verifying Wait-Freedom for Concurrent Higher-Order Programs. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 20:1-20:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ECOOP.2026.20

Author Details

Egor Namakonov
  • Aarhus University, Denmark
Lars Birkedal
  • Aarhus University, Denmark
Amin Timany
  • Aarhus University, Denmark

Funding

This work was supported in part by a Villum Investigator grant (VIL73403) and Center for Basic Research in Program Verification (CPV, 25804), from Villum Fonden. This work was co-funded by the European Union (ERC, CHORDS, 101096090). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

Acknowledgements

We thank the anonymous reviewers for the feedback that helped to make our work more accessible, and Justus Fasse for the discussions on the specification style.

Supplementary Materials

References

  1. Andrew W. Appel. Verified software toolchain. In Gilles Barthe, editor, Programming Languages and Systems, pages 1-17, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  2. Lars Birkedal and Ales Bizjak. Lecture notes on Iris: Higher-order concurrent separation logic, 2017. URL: http://iris-project.org/tutorial-pdfs/iris-lecture-notes.pdf.
  3. Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. Theorems for free from separation logic specifications. Proc. ACM Program. Lang., 5(ICFP), August 2021. URL: https://doi.org/10.1145/3473586.
  4. Fabian Bläse. Non-blocking synchronization in operating systems, 2021. URL: https://www4.cs.fau.de/Lehre/WS20/MS_AKSS/arbeiten/paper_blaese_final.pdf.
  5. Hagit Brit and Shlomo Moran. Wait-freedom vs. bounded wait-freedom in public data structures (extended abstract). In James H. Anderson, David Peleg, and Elizabeth Borowsky, editors, Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, Los Angeles, California, USA, August 14-17, 1994, PODC '94, pages 52-60, New York, NY, USA, 1994. ACM. URL: https://doi.org/10.1145/197917.197950.
  6. Andreia Correia, Pedro Ramalhete, and Pascal Felber. A wait-free universal construction for large objects. In Rajiv Gupta and Xipeng Shen, editors, PPoPP '20: 25th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, San Diego, California, USA, February 22-26, 2020, PPoPP '20, pages 102-116, New York, NY, USA, 2020. ACM. URL: https://doi.org/10.1145/3332466.3374523.
  7. Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. Tada: A logic for time and data abstraction. In Richard E. Jones, editor, ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, July 28 - August 1, 2014. Proceedings, Lecture Notes in Computer Science, pages 207-231. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44202-9_9.
  8. Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. Modular termination verification for non-blocking concurrency. In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 176-201. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_8.
  9. Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. In Paul Hudak and Stephanie Weirich, editors, Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 143-156. ACM, 2010. URL: https://doi.org/10.1145/1863543.1863566.
  10. Panagiota Fatourou and Nikolaos D. Kallimanis. A highly-efficient wait-free universal construction. In Rajmohan Rajaraman and Friedhelm Meyer auf der Heide, editors, SPAA 2011: Proceedings of the 23rd Annual ACM Symposium on Parallelism in Algorithms and Architectures, San Jose, CA, USA, June 4-6, 2011 (Co-located with FCRC 2011), SPAA '11, pages 325-334, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/1989493.1989549.
  11. Panagiota Fatourou, Nikolaos D. Kallimanis, and Eleni Kanellou. An Efficient Universal Construction for Large Objects. In Pascal Felber, Roy Friedman, Seth Gilbert, and Avery Miller, editors, 23rd International Conference on Principles of Distributed Systems (OPODIS 2019), volume 153 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:15, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.OPODIS.2019.18.
  12. Aïna LinnGeorges. Designing and proving robust safety of efficient capability machine programs, July 2023. Google Scholar
  13. Seep Goel, Pooja Aggarwal, and Smruti R. Sarangi. A wait-free stack. In Nikolaj S. Bjørner, Sanjiva Prasad, and Laxmi Parida, editors, Distributed Computing and Internet Technology - 12th International Conference, ICDCIT 2016, Bhubaneswar, India, January 15-18, 2016, Proceedings, Lecture Notes in Computer Science, pages 43-55. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-28034-9_6.
  14. Alexey Gotsman, Byron Cook, Matthew J. Parkinson, and Viktor Vafeiadis. Proving that non-blocking algorithms don't block. In Zhong Shao and Benjamin C. Pierce, editors, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, pages 16-28. ACM, 2009. URL: https://doi.org/10.1145/1480881.1480886.
  15. Maurice Herlihy. Wait-free synchronization. ACM Trans. Program. Lang. Syst., 13(1):124-149, January 1991. URL: https://doi.org/10.1145/114005.102808.
  16. Maurice Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, July 1990. URL: https://doi.org/10.1145/78969.78972.
  17. Bart Jacobs and Frank Piessens. Expressive modular fine-grained concurrency specification. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, POPL '11, pages 271-282, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/1926385.1926417.
  18. Prasad Jayanti and Srdjan Petrovic. Logarithmic-time single deleter, multiple inserter wait-free queues and stacks. In Ramaswamy Ramanujam and Sandeep Sen, editors, FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, Hyderabad, India, December 15-18, 2005, Proceedings, Lecture Notes in Computer Science, pages 408-419. Springer, 2005. URL: https://doi.org/10.1007/11590156_33.
  19. Cliff B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5(4):596-619, October 1983. URL: https://doi.org/10.1145/69575.69577.
  20. 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.
  21. 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), December 2019. URL: https://doi.org/10.1145/3371113.
  22. 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.
  23. Alex Kogan and Erez Petrank. Wait-free queues with multiple enqueuers and dequeuers. SIGPLAN Not., pages 223-234, 2011. URL: https://doi.org/10.1145/1941553.1941585.
  24. Alex Kogan and Erez Petrank. A methodology for creating fast wait-free data structures. SIGPLAN Not., pages 141-150, 2012. URL: https://doi.org/10.1145/2145816.2145835.
  25. Pierre LaBorde, Steven D. Feldman, and Damian Dechev. A wait-free hash map. Int. J. Parallel Program., 45(3):421-448, June 2017. URL: https://doi.org/10.1007/s10766-015-0376-3.
  26. Hongjin Liang and Xinyu Feng. A program logic for concurrent objects under fair scheduling. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, POPL '16, pages 385-399, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2837614.2837635.
  27. Hongjin Liang, Xinyu Feng, and Zhong Shao. Compositional verification of termination-preserving refinement of concurrent programs. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2603088.2603123.
  28. Maged M. Michael and Michael L. Scott. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In James E. Burns and Yoram Moses, editors, Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, Philadelphia, Pennsylvania, USA, May 23-26, 1996, PODC '96, pages 267-275, New York, NY, USA, 1996. ACM. URL: https://doi.org/10.1145/248052.248106.
  29. Egor Namakonov, Lars Birkedal, and Amin Timany. Verifying wait-freedom for concurrent higher-order programs (artifact), April 2026. URL: https://zenodo.org/records/19607892/files/artifact.pdf.
  30. Egor Namakonov, Lars Birkedal, and Amin Timany. Verifying wait-freedom for concurrent higher-order programs (technical appendix), April 2026. URL: https://zenodo.org/records/19607892/files/paper-appendix.pdf.
  31. Egor Namakonov, Justus Fasse, Bart Jacobs, Lars Birkedal, and Amin Timany. Lawyer: Modular obligations-based liveness reasoning in higher-order impredicative concurrent separation logic. Proc. ACM Program. Lang., 10(OOPSLA1), April 2026. URL: https://doi.org/10.1145/3798240.
  32. Christina Peterson, Victor Cook, and Damian Dechev. Practical progress verification of descriptor-based non-blocking data structures. In 2019 IEEE 27th International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS), pages 83-93, 2019. URL: https://doi.org/10.1109/MASCOTS.2019.00019.
  33. Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. Transfinite iris: resolving an existential dilemma of step-indexed separation logic. 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, 2021, pages 80-95. ACM, 2021. URL: https://doi.org/10.1145/3453483.3454031.
  34. David Swasey, Deepak Garg, and Derek Dreyer. Robust and compositional verification of object capability patterns. Proc. ACM Program. Lang., 1(OOPSLA), October 2017. URL: https://doi.org/10.1145/3133913.
  35. Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, and Lars Birkedal. Trillium: Higher-order concurrent and distributed separation logic for intensional refinement. Proc. ACM Program. Lang., 8(POPL), January 2024. URL: https://doi.org/10.1145/3632851.
  36. Shahar Timnat, Anastasia Braginsky, Alex Kogan, and Erez Petrank. Wait-free linked-lists. In J. Ramanujam and P. Sadayappan, editors, Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2012, New Orleans, LA, USA, February 25-29, 2012, pages 309-310. ACM, 2012. URL: https://doi.org/10.1145/2145816.2145869.
  37. Viktor Vafeiadis. Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, UK, July 2008. URL: https://doi.org/10.48456/tr-726.
  38. Martin T. Vechev and Eran Yahav. Deriving linearizable fine-grained concurrent objects. In Rajiv Gupta and Saman P. Amarasinghe, editors, Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, pages 125-135. ACM, 2008. URL: https://doi.org/10.1145/1375581.1375598.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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