Document Open Access Logo

Foundational and Compositional Verification of Layered Concurrent Objects

Authors Yicheng Ni , Yuting Wang

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2026.21.pdf
  • Filesize: 1.84 MB
  • 31 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Parallel computing models
  • Theory of computation → Program verification
  • Theory of computation → Operational semantics
Keywords
  • Concurrency
  • Compositional Verification

Metrics

Abstract

Compositionality is essential for managing complexity in verification of concurrent programs, especially when proof certificates are needed. An effective verification scheme is to divide programs into abstraction layers and verify by composing refinements between layers. However, vanilla verified layers come with global states which severely limit their extensibility. This problem may be solved by dividing a layer into objects with encapsulated local states. Although the idea has been successfully realized in the sequential setting, it remains unclear if it also works in a concurrent setting where function calls across layers are no longer atomic steps and foundational proofs are needed.
We propose an approach to foundational and compositional verification of concurrent objects organized into multiple layers. The central idea is to represent concurrent objects as open labeled transition systems with encapsulated threads and to adopt trace refinements as a uniform notion of functional correctness which supports both vertical composition (layered refinement) and horizontal composition (extension of layer interfaces). Due to the operational nature of transition systems, it is straightforward to adopt traditional simulation techniques to produce foundational proof certificates. We implement this framework in the Rocq theorem prover and demonstrate its capability in foundational and compositional verification by verifying non-trivial lock-free concurrent data structures.

Cite As Get BibTex

Yicheng Ni and Yuting Wang. Foundational and Compositional Verification of Layered Concurrent Objects. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 21:1-21:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ECOOP.2026.21

Author Details

Yicheng Ni
  • Shanghai Jiao Tong University, School of Computer Science, China
Yuting Wang
  • Shanghai Jiao Tong University, School of Computer Science, China

Funding

This work was supported by the National Natural Science Foundation of China (NSFC) under Grant No. 62372290, W2421088 and 62002217.

Supplementary Materials

References

  1. Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theor. Comput. Sci., 82(2):253-284, 1991. URL: https://doi.org/10.1016/0304-3975(91)90224-P.
  2. Andrew Appel. Verified software toolchain. In Gilles Barthe, editor, Proc. 20th European Symposium on Programming (ESOP'11), volume 6602 of LNCS, pages 1-17. Springer, Saarbrucken, Germany, 2011. URL: https://doi.org/10.1007/978-3-642-19718-5_1.
  3. Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Proc. 4th Symp on Formal Methods for Components and Objects, 2005. URL: https://doi.org/10.1007/11804192_17.
  4. Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang. Concurrent library correctness on the tso memory model. In Helmut Seidl, editor, Programming Languages and Systems, pages 87-107, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-28869-2_5.
  5. Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Argosy: verifying layered storage systems with recovery refinement. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pages 1054-1068, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3314221.3314585.
  6. Nicolas Chappe. A family of sims with diverging interests. Proc. ACM Program. Lang., 10(POPL), January 2026. URL: https://doi.org/10.1145/3776714.
  7. Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Using crash hoare logic for certifying the fscq file system. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP '15, pages 18-37, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2815400.2815402.
  8. Robert Colvin and Lindsay Groves. Formal verification of an array-based nonblocking queue. In Proceedings of the 10th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS '05, pages 507-516, USA, 2005. IEEE Computer Society. URL: https://doi.org/10.1109/ICECCS.2005.49.
  9. Zhenyang Dai, Shuang Liu, Vilhelm Sjoberg, Xupeng Li, Yu Chen, Wenhao Wang, Yuekai Jia, Sean Noble Anderson, Laila Elbeheiry, Shubham Sondhi, Yu Zhang, Zhaozhong Ni, Shoumeng Yan, Ronghui Gu, and Zhengyu He. Verifying rust implementation of page tables in a software enclave hypervisor. In Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2, ASPLOS '24, pages 1218-1232, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3620665.3640398.
  10. Ian Dardik and Eunsuk Kang. Compositional inductive invariant inference via assume-guarantee reasoning, 2025. URL: https://doi.org/10.48550/arXiv.2509.06250.
  11. John Derrick and Eerke Boiten. Labeled Transition Systems and Their Refinement, pages 3-26. Springer International Publishing, Cham, 2018. URL: https://doi.org/10.1007/978-3-319-92711-4_1.
  12. John Derrick, Gerhard Schellhorn, and Heike Wehrheim. Mechanizing a correctness proof for a lock-free concurrent stack. In Gilles Barthe and Frank S. de Boer, editors, Formal Methods for Open Object-Based Distributed Systems, pages 78-95, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-68863-1_6.
  13. Brijesh Dongol and John Derrick. Verifying linearisability: A comparative survey. ACM Comput. Surv., 48(2), September 2015. URL: https://doi.org/10.1145/2796550.
  14. Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi, and Serdar Tasiran. Simplifying linearizability proofs with reduction and abstraction. In Proc. TACAS'10, pages 296-311, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_25.
  15. Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, and Hongseok Yang. Abstraction for concurrent objects. Theor. Comput. Sci., 411(51-52):4379-4398, 2010. URL: https://doi.org/10.1016/j.tcs.2010.09.021.
  16. Lean FRO. The Lean language, 2025. URL: https://lean-lang.org/.
  17. Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. Simuliris: a separation logic framework for verifying concurrent program optimizations. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498689.
  18. Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of fine-grained concurrency. Annals of Pure and Applied Logic, 151(2-3):89-114, 2008. URL: https://doi.org/10.1016/j.apal.2007.10.005.
  19. Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, and Ilya Sergey. Foundational multi-modal program verifiers. Proc. ACM Program. Lang., 10(POPL), January 2026. URL: https://doi.org/10.1145/3776719.
  20. Alexey Gotsman and Hongseok Yang. Liveness-preserving atomicity abstraction. In Proceedings of the 38th International Conference on Automata, Languages and Programming - Volume Part II, ICALP'11, pages 453-465, Berlin, Heidelberg, 2011. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-22012-8_36.
  21. Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan(Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. Deep specifications and certified abstraction layers. In Sriram K. Rajamani and David Walker, editors, Proc. 42nd ACM Symposium on Principles of Programming Languages (POPL'15), pages 595-608, New York, NY, USA, 2015. ACM. URL: https://doi.org/10.1145/2775051.2676975.
  22. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proc. 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI'16), pages 653-669, GA, 2016. USENIX Association. URL: https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu.
  23. Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjober, Hao Chen, David Costanzo, and Tahnia Ramananandro. Certified concurrent abstraction layers. In Jeffrey S. Foster and Dan Grossman, editors, Proc. 2018 ACM Conference on Programming Language Design and Implementation (PLDI'18), pages 646-661, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3192366.3192381.
  24. Maurice Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, 1990. URL: https://doi.org/10.1145/78969.78972.
  25. Atalay Mert Ileri, Nickolai Zeldovich, Adam Chlipala, and Frans Kaashoek. Probability from possibility: Probabilistic confidentiality for storage systems under nondeterminism. In 2024 IEEE 37th Computer Security Foundations Symposium (CSF), pages 96-111, 2024. URL: https://doi.org/10.1109/CSF61375.2024.00041.
  26. Prasad Jayanti, Siddhartha Jayanti, Ugur Y. 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.
  27. Cliff B Jones. Specification and design of (parallel) programs. In 9th IFIP World Computer Congress (Information Processing 83). Newcastle University, 1983. URL: https://api.semanticscholar.org/CorpusID:38308402.
  28. Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. Higher-order ghost state. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, pages 256-269, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2951913.2951943.
  29. Ralf Jung, David Swasey, Filip Sieczkowski, Ksper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Proc. 42nd ACM Symposium on Principles of Programming Languages (POPL'15), pages 637-650, 2015. URL: https://doi.org/10.1145/2775051.2676980.
  30. Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. A promising semantics for relaxed-memory concurrency. In Giuseppe Castagna and Andrew D. Gordon, editors, Proc. 44th ACM Symposium on Principles of Programming Languages (POPL'17), pages 175-189, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3009837.3009850.
  31. Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew Parkinson. Proving linearizability using partial orders. In Hongseok Yang, editor, Programming Languages and Systems, pages 639-667, Heidelberg, 2017. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-54434-1_24.
  32. Artem Khyzha and Ori Lahav. Abstraction for crash-resilient objects. In Ilya Sergey, editor, Programming Languages and Systems, pages 262-289, Cham, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-99336-8_10.
  33. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, et al. seL4: Formal verification of an OS kernel. In SOSP'09, pages 207-220, October 2009. URL: https://doi.org/10.1145/1629575.1629596.
  34. Bernhard Kragl and Shaz Qadeer. Layered concurrent programs. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification, pages 79-102, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-96145-3_5.
  35. Bernhard Kragl and Shaz Qadeer. The civl verifier. In 2021 Formal Methods in Computer Aided Design (FMCAD), pages 143-152, 2021. URL: https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23.
  36. Bernhard Kragl, Shaz Qadeer, and Thomas A. Henzinger. Refinement for structured concurrent programs. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification, pages 275-298, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-53288-8_14.
  37. Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872-923, 1994. URL: https://doi.org/10.1145/177492.177726.
  38. Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, and Viktor Vafeiadis. Promising 2.0: Global optimizations in relaxed memory concurrency. In Proc. 2020 ACM Conference on Programming Language Design and Implementation (PLDI'20), pages 362-376, New York, NY, USA, 2020. ACM. URL: https://doi.org/10.1145/3385412.3386010.
  39. Paul Blain Levy and Sam Staton. Transition systems over games. In Thomas A. Henzinger and Dale Miller, editors, 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, Vienna, Austria, July 14 - 18, 2014, pages 64:1-64:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603150.
  40. Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh. Spoq: Scaling Machine-Checkable systems verification in coq. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23), pages 851-869, 2023. URL: https://www.usenix.org/conference/osdi23/presentation/li-xupeng.
  41. Yang Liu, Wei Chen, Yanhong A. Liu, and Jun Sun. Model checking linearizability via refinement. In Ana Cavalcanti and Dennis R. Dams, editors, FM 2009: Formal Methods, pages 321-337, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-05089-3_21.
  42. Nancy A. Lynch and Mark R. Tuttle. An introduction to input/output automata. CWI quarterly, 2:219-246, 1989. URL: https://api.semanticscholar.org/CorpusID:10292247.
  43. Nancy A. Lynch and Frits W. Vaandrager. Forward and backward simulations: I. Untimed systems. Inf. Comput., 121(2):214-233, 1995. URL: https://doi.org/10.1006/inco.1995.1134.
  44. Ike Mulder, Robbert Krebbers, and Herman Geuvers. Diaframe: automated verification of fine-grained concurrent programs in iris. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022, pages 809-824, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3519939.3523432.
  45. Peter W. O'Hearn. Resources, concurrency and local reasoning. In CONCUR'04, pages 49-67, 2004. URL: https://doi.org/10.1016/j.tcs.2006.12.035.
  46. 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.
  47. Susan Owicki and David Gries. Verifying properties of parallel programs: an axiomatic approach. Commun. ACM, 19(5):279-285, May 1976. URL: https://doi.org/10.1145/360051.360224.
  48. Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, and Jeehoon Kang. A proof recipe for linearizability in relaxed memory separation logic. Proc. ACM Program. Lang., 8(PLDI), June 2024. URL: https://doi.org/10.1145/3656384.
  49. George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey. Veil: A framework for automated and interactive verification of transition systems. In Ruzica Piskac and Zvonimir Rakamarić, editors, Computer Aided Verification, pages 26-41, Cham, 2025. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-98682-6_2.
  50. Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis. On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290381.
  51. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS'02, pages 55-74, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  52. Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell. Islaris: verification of machine code against authoritative isa semantics. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022, pages 825-840, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3519939.3523434.
  53. Abhishek Kr Singh and Ori Lahav. An operational approach to library abstraction under relaxed memory concurrency. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571246.
  54. 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 Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pages 80-95, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3453483.3454031.
  55. Simon Spies, Niklas Mück, Haoyi Zeng, Michael Sammler, Andrea Lattuada, Peter Müller, and Derek Dreyer. Destabilizing iris. Proc. ACM Program. Lang., 9(PLDI), June 2025. URL: https://doi.org/10.1145/3729284.
  56. Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, and Ronghui Gu. Formal verification of a multiprocessor hypervisor on arm relaxed memory hardware. In Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles, SOSP '21, pages 866-881, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3477132.3483560.
  57. Rocq Development Team. The rocq prover. version 9.0.0, released March 12, 2025., 2025. URL: https://rocq-prover.org/.
  58. Martin Thompson, Dave Farley, Michael Barker, Patricia Gee, and Andrew Stewart. Disruptor: High performance alternative to bounded queues for, 2011. Google Scholar
  59. 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.
  60. Xiaoxiao Yang, Joost-Pieter Katoen, Huimin Lin, Gaoang Liu, and Hao Wu. Branching bisimulation and concurrent object verification. In 2018 48th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pages 267-278, 2018. URL: https://doi.org/10.1109/DSN.2018.00037.
  61. Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey. Compositional verification of composite byzantine protocols. In Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, CCS '24, pages 34-48, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3658644.3690355.
  62. Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, and Qinxiang Cao. Vst-a: A foundationally sound annotation verifier. Proc. ACM Program. Lang., 8(POPL), January 2024. URL: https://doi.org/10.1145/3632911.
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