Document Open Access Logo

A Complete Program Logic for Compositional Linearizability

Authors Eashan Hatti , Arthur Oliveira Vale , Zhongye Wang , Yueyang Feng , Zhong Shao

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2026.11.pdf
  • Filesize: 1.53 MB
  • 28 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Computing methodologies → Concurrent computing methodologies
  • Theory of computation → Programming logic
Keywords
  • Program Logic
  • Rely-Guarantee
  • Linearizability
  • Compositional Verification
  • Concurrency

Metrics

Abstract

We present Linearizability Hoare Logic (LHL), the first mechanized, sound, and complete program logic for atomic, set, and interval linearizability. We achieve this by showing soundness and completeness of LHL w.r.t. a more general criterion, compositional linearizability, which subsumes all three criteria. We showcase the expressivity of LHL by verifying an exchanger with a set linearizable specification, the elimination-backoff stack built above the exchanger, a lock with an atomic linearized specification, and a write-snapshot object with an interval linearizable specification.
Together with LHL we formalize a modular verification framework for concurrent components based on the theory of compositional linearizability. This allows us to specify components at a high level of abstraction and granularity, and then assemble them into large systems that are correct by construction. As a showcase, we verify the elimination-backoff stack modularly by verifying each of its sub-components against their linearized specifications and then linking them together.

Cite As Get BibTex

Eashan Hatti, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, and Zhong Shao. A Complete Program Logic for Compositional Linearizability. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 11:1-11:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ECOOP.2026.11

Author Details

Eashan Hatti
  • Yale University, New Haven, CT, USA
Arthur Oliveira Vale
  • Yale University, New Haven, CT, USA
Zhongye Wang
  • Yale University, New Haven, CT, USA
Yueyang Feng
  • Yale University, New Haven, CT, USA
Zhong Shao
  • Yale University, New Haven, CT, USA

Funding

This work is supported in part by NSF grants 2019285, 2313433, 2442888, and by the Defense Advanced Research Projects Agency (DARPA) under Agreement No. HR00112590130. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the funding agencies.

Acknowledgements

We would like to thank the anonymous reviewers and artifact evaluation committee for their thoughtful feedback and time spent reviewing our work.

Supplementary Materials

References

  1. Nick Benton. Simple relational correctness proofs for static analyses and program transformations. ACM SIGPLAN Notices, 39(1):14-25, 2004. URL: https://doi.org/10.1145/964001.964003.
  2. Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. Theorems for free from separation logic specifications. Proceedings of the ACM on Programming Languages, 5(ICFP):1-29, 2021. URL: https://doi.org/10.1145/3473586.
  3. Elizabeth Borowsky and Eli Gafni. Immediate atomic snapshots and fast renaming (extended abstract). In Jim Anderson and Sam Toueg, editors, Proceedings of the Twelth Annual ACM Symposium on Principles of Distributed Computing, Ithaca, New York, USA, August 15-18, 1993, pages 41-51. ACM, 1993. URL: https://doi.org/10.1145/164051.164056.
  4. Jeremy S Bradbury, James R Cordy, and Juergen Dingel. Mutation operators for concurrent java (j2se 5.0). In Second Workshop on Mutation Analysis (Mutation 2006-ISSRE Workshops 2006), pages 11-11. IEEE, 2006. Google Scholar
  5. Armando Castañeda, Sergio Rajsbaum, and Michel Raynal. Specifying concurrent problems: Beyond linearizability and up to tasks. In Proceedings of the 29th International Symposium on Distributed Computing - Volume 9363, DISC 2015, pages 420-435, Berlin, Heidelberg, 2015. Springer-Verlag. URL: https://doi.org/10.1007/978-3-662-48653-5_28.
  6. Robert Colvin and Lindsay Groves. A scalable lock-free stack algorithm and its verification. In Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), pages 339-348. IEEE, 2007. URL: https://doi.org/10.1109/SEFM.2007.2.
  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, volume 8586 of Lecture Notes in Computer Science, pages 207-231. Springer, Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44202-9_9.
  8. Mike Dodds, Andreas Haas, and Christoph M. Kirsch. A scalable, correct time-stamped stack. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 233-246, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2676726.2676963.
  9. Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, and Hongseok Yang. Abstraction for concurrent objects. In Giuseppe Castagna, editor, Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5502 of Lecture Notes in Computer Science, pages 252-266, Berlin, Heidelberg, 2009. Springer. URL: https://doi.org/10.1007/978-3-642-00590-9_19.
  10. Dan Frumin, Robbert Krebbers, and Lars Birkedal. Reloc: A mechanised relational logic for fine-grained concurrency. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 442-451. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209174.
  11. Dan Frumin, Robbert Krebbers, and Lars Birkedal. Reloc reloaded: A mechanized relational logic for fine-grained concurrency and logical atomicity. Log. Methods Comput. Sci., 17(3), 2021. URL: https://doi.org/10.46298/lmcs-17(3:9)2021.
  12. Éric Goubault, Jérémy Ledent, and Samuel Mimram. Concurrent specifications beyond linearizability. In Jiannong Cao, Faith Ellen, Luís Rodrigues, and Bernardo Ferreira, editors, 22nd International Conference on Principles of Distributed Systems, OPODIS 2018, Hong Kong, December 17-19, 2018, volume 125 of LIPIcs, pages 28:1-28:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.OPODIS.2018.28.
  13. Eashan Hatti, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, and Zhong Shao. Linearizability Hoare Logic. Software, NSF 2019285, NSF 2313433, NSF 2442888, DARPA Agreement No. HR00112590130, (visited on 2026-06-10). URL: https://github.com/ehatti/LHL/tree/ecoop-camera-ready
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26388
  14. Eashan Hatti, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, and Zhong Shao. A complete program logic for compositional linearizability. Technical Report YALEU/DCS/TR-1577, Yale University, 2026. URL: https://flint.cs.yale.edu/publications/lhl.html.
  15. Danny Hendler, Nir Shavit, and Lena Yerushalmi. A scalable lock-free stack algorithm. In Proceedings of the sixteenth annual ACM symposium on Parallelism in algorithms and architectures, pages 206-215, 2004. URL: https://doi.org/10.1145/1007912.1007944.
  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. Prasad Jayanti, Siddhartha Jayanti, Ugur Yavuz, and Lizzie Hernandez. A universal, sound, and complete forward reasoning technique for machine-verified proofs of linearizability. Proc. ACM Program. Lang., 8(POPL), January 2024. URL: https://doi.org/10.1145/3632924.
  18. 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.
  19. 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. Journal of Functional Programming, 28:e20, 2018. URL: https://doi.org/10.1017/S0956796818000151.
  20. Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. The future is ours: prophecy variables in separation logic. Proceedings of the ACM on Programming Languages, 4(POPL):1-32, 2019. URL: https://doi.org/10.1145/3371113.
  21. Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew Parkinson. Proving linearizability using partial orders. In 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 26, pages 639-667. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_24.
  22. Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic. C4: verified transactional objects. Proc. ACM Program. Lang., 6(OOPSLA1), April 2022. URL: https://doi.org/10.1145/3527324.
  23. Hongjin Liang and Xinyu Feng. Modular verification of linearizability with non-fixed linearization points. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 459-470, 2013. URL: https://doi.org/10.1145/2491956.2462189.
  24. Nancy A. Lynch and Frits W. Vaandrager. Forward and backward simulations, II: timing-based systems. Inf. Comput., 128(1):1-25, July 1996. URL: https://doi.org/10.1006/inco.1996.0060.
  25. Gil Neiger. Set-linearizability. In Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, PODC '94, page 396, New York, NY, USA, 1994. Association for Computing Machinery. URL: https://doi.org/10.1145/197917.198176.
  26. Arthur Oliveira Vale, Zhong Shao, and Yixuan Chen. A compositional theory of linearizability. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571231.
  27. Arthur Oliveira Vale, Zhong Shao, and Yixuan Chen. A compositional theory of linearizability. J. ACM, 71(2), April 2024. URL: https://doi.org/10.1145/3643668.
  28. Gerhard Schellhorn, John Derrick, and Heike Wehrheim. A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Logic, 15(4), September 2014. URL: https://doi.org/10.1145/2629496.
  29. Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, and Germán Andrés Delbianco. Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. ACM SIGPLAN Notices, 51(10):92-110, 2016. URL: https://doi.org/10.1145/2983990.2983999.
  30. Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer. Conditional contextual refinement. Proceedings of the ACM on Programming Languages, 7(POPL):1121-1151, 2023. URL: https://doi.org/10.1145/3571232.
  31. Aaron Turon, Derek Dreyer, and Lars Birkedal. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In Proceedings of the 18th ACM SIGPLAN international conference on Functional programming, pages 377-390, 2013. URL: https://doi.org/10.1145/2500365.2500600.
  32. Viktor Vafeiadis. Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, UK, July 2008. URL: https://doi.org/10.48456/tr-726.
  33. Simon Friis Vindum, Dan Frumin, and Lars Birkedal. Mechanized verification of a fine-grained concurrent queue from meta’s folly library. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 100-115, 2022. URL: https://doi.org/10.1145/3497775.3503689.
  34. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371119.
  35. Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li. A practical verification framework for preemptive os kernels. In International Conference on Computer Aided Verification, pages 59-79. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_4.
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