{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:11:08Z","timestamp":1750219868185,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>\n            Writing concurrent code that is both correct and efficient is notoriously difficult. Thus, programmers often prefer to use synchronization abstractions, which render code simpler and easier to reason about. Despite a wealth of work on this topic, there is still a gap between the rich semantics provided by synchronization abstractions in modern programming languages\u2014specifically,\n            <jats:italic>fair<\/jats:italic>\n            FIFO ordering of synchronization requests and support for\n            <jats:italic>abortable<\/jats:italic>\n            operations\u2014and frameworks for implementing it correctly and efficiently. Supporting such semantics is critical given the rising popularity of constructs for asynchronous programming, such as coroutines, which abort frequently and are cheaper to suspend and resume compared to native threads.\n          <\/jats:p>\n          <jats:p>\n            This paper introduces a new framework called CancellableQueueSynchronizer (CQS), which enables simple yet efficient implementations of a wide range of fair and abortable synchronization primitives: mutexes, semaphores, barriers, count-down latches, and blocking pools. Our main contribution is algorithmic, as implementing both fairness and abortability efficiently at this level of generality is non-trivial. Importantly, all our algorithms, including the CQS framework and the primitives built on top of it, come with\n            <jats:italic>formal proofs<\/jats:italic>\n            in the Iris framework for Coq for many of their properties. These proofs are modular, so it is easy to show correctness for new primitives implemented on top of CQS. From a practical perspective, implementation of CQS for native threads on the JVM improves throughput by up to two orders of magnitude over Java\u2019s AbstractQueuedSynchronizer, the only practical abstraction offering similar semantics. Further, we successfully integrated CQS as a core component of the popular Kotlin Coroutines library, validating the framework\u2019s practical impact and expressiveness in a real-world environment. In sum, CancellableQueueSynchronizer is the first framework to combine expressiveness with formal guarantees and solid practical performance. Our approach should be extensible to other languages and families of synchronization primitives.\n          <\/jats:p>","DOI":"10.1145\/3591230","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"244-266","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["CQS: A Formally-Verified Framework for Fair and Abortable Synchronization"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0491-3953","authenticated-orcid":false,"given":"Nikita","family":"Koval","sequence":"first","affiliation":[{"name":"JetBrains, Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4803-5740","authenticated-orcid":false,"given":"Dmitry","family":"Khalanskiy","sequence":"additional","affiliation":[{"name":"JetBrains, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3650-940X","authenticated-orcid":false,"given":"Dan","family":"Alistarh","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2021. JMH - Java Microbenchmark Harness. https:\/\/openjdk.java.net\/projects\/code-tools\/jmh\/ \t\t\t\t  2021. JMH - Java Microbenchmark Harness. https:\/\/openjdk.java.net\/projects\/code-tools\/jmh\/"},{"key":"e_1_2_1_2_1","unstructured":"2022. Kotlin Coroutines. https:\/\/github.com\/Kotlin\/kotlin-coroutines \t\t\t\t  2022. Kotlin Coroutines. https:\/\/github.com\/Kotlin\/kotlin-coroutines"},{"key":"e_1_2_1_3_1","unstructured":"2023. CQS Formal Proofs. https:\/\/github.com\/Kotlin\/kotlinx.coroutines\/tree\/cqs-proofs \t\t\t\t  2023. CQS Formal Proofs. https:\/\/github.com\/Kotlin\/kotlinx.coroutines\/tree\/cqs-proofs"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3212734.3212759"},{"key":"e_1_2_1_5_1","unstructured":"Various authors. 2022. https:\/\/gitlab.mpi-sws.org\/iris\/examples\/-\/tree\/0260d3d08e2f56bbccd44c3d56436baea30da4c9\/theories\/logatom \t\t\t\t  Various authors. 2022. https:\/\/gitlab.mpi-sws.org\/iris\/examples\/-\/tree\/0260d3d08e2f56bbccd44c3d56436baea30da4c9\/theories\/logatom"},{"key":"e_1_2_1_6_1","volume-title":"European Conference on Object-Oriented Programming. 233\u2013257","author":"Bierman Gavin","year":"2012","unstructured":"Gavin Bierman , Claudio Russo , Geoffrey Mainland , Erik Meijer , and Mads Torgersen . 2012 . Pause\u2019n\u2019Play: Formalizing Asynchronous C# . In European Conference on Object-Oriented Programming. 233\u2013257 . Gavin Bierman, Claudio Russo, Geoffrey Mainland, Erik Meijer, and Mads Torgersen. 2012. Pause\u2019n\u2019Play: Formalizing Asynchronous C#. In European Conference on Object-Oriented Programming. 233\u2013257."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503681"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 15th Symposium on Operating Systems Design and Implementation (OSDI). Virtual, 423\u2013439","author":"Chajed Tej","year":"2021","unstructured":"Tej Chajed , Joseph Tassarotti , Mark Theng , Ralf Jung , M Frans Kaashoek , and Nickolai Zeldovich . 2021 . GoJournal: a verified, concurrent, crash-safe journaling system . In Proceedings of the 15th Symposium on Operating Systems Design and Implementation (OSDI). Virtual, 423\u2013439 . Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M Frans Kaashoek, and Nickolai Zeldovich. 2021. GoJournal: a verified, concurrent, crash-safe journaling system. In Proceedings of the 15th Symposium on Operating Systems Design and Implementation (OSDI). Virtual, 423\u2013439."},{"key":"e_1_2_1_9_1","volume-title":"Safe Session-Based Asynchronous Coordination in Rust. In International Conference on Coordination Languages and Models. 80\u201389","author":"Cutner Zak","year":"2021","unstructured":"Zak Cutner and Nobuko Yoshida . 2021 . Safe Session-Based Asynchronous Coordination in Rust. In International Conference on Coordination Languages and Models. 80\u201389 . Zak Cutner and Nobuko Yoshida. 2021. Safe Session-Based Asynchronous Coordination in Rust. In International Conference on Coordination Languages and Models. 80\u201389."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-010-0096-2"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the ACM on Programming Languages, 4, POPL","author":"Dang Hoang-Hai","year":"2019","unstructured":"Hoang-Hai Dang , Jacques-Henri Jourdan , Jan-Oliver Kaiser , and Derek Dreyer . 2019 . RustBelt Meets Relaxed Memory . Proceedings of the ACM on Programming Languages, 4, POPL (2019), 1\u201329. Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer. 2019. RustBelt Meets Relaxed Memory. Proceedings of the ACM on Programming Languages, 4, POPL (2019), 1\u201329."},{"volume-title":"Pioneers and Their Contributions to Software Engineering","author":"Dijkstra Edsger W","key":"e_1_2_1_12_1","unstructured":"Edsger W Dijkstra . 2001. Solution of a Problem in Concurrent Programming Control . In Pioneers and Their Contributions to Software Engineering . Springer , 289\u2013294. Edsger W Dijkstra. 2001. Solution of a Problem in Concurrent Programming Control. In Pioneers and Their Contributions to Software Engineering. Springer, 289\u2013294."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087801.3087837"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.03.002"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3040220"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/872035.872079"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693179"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the ACM on Programming Languages, 2, POPL","author":"Jung Ralf","year":"2017","unstructured":"Ralf Jung , Jacques-Henri Jourdan , Robbert Krebbers , and Derek Dreyer . 2017 . RustBelt: Securing the Foundations of the Rust Programming Language . Proceedings of the ACM on Programming Languages, 2, POPL (2017), 1\u201334. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: Securing the Foundations of the Rust Programming Language. Proceedings of the ACM on Programming Languages, 2, POPL (2017), 1\u201334."},{"key":"e_1_2_1_19_1","volume-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung , Robbert Krebbers , Jacques-Henri Jourdan , Ale\u0161 Bizjak , Lars Birkedal , and Derek Dreyer . 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 ( 2018 ). Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 (2018)."},{"key":"e_1_2_1_20_1","unstructured":"Gilles Kahn and David MacQueen. 1976. Coroutines and Networks of Parallel Processes. \t\t\t\t  Gilles Kahn and David MacQueen. 1976. Coroutines and Networks of Parallel Processes."},{"key":"e_1_2_1_21_1","volume-title":"Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming (ECOOP","author":"Kaiser Jan-Oliver","year":"2017","unstructured":"Jan-Oliver Kaiser , Hoang-Hai Dang , Derek Dreyer , Ori Lahav , and Viktor Vafeiadis . 2017 . Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming (ECOOP 2017)."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/355592.365595"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29400-7_23"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3572848.3577481"},{"key":"e_1_2_1_25_1","unstructured":"Nikita Koval Dmitry Khalanskiy and Dan Alistarh. 2023. A Formally-Verified Framework for Fair Synchronization in Kotlin Coroutines. arxiv:2111.12682. \t\t\t\t  Nikita Koval Dmitry Khalanskiy and Dan Alistarh. 2023. A Formally-Verified Framework for Fair Synchronization in Kotlin Coroutines. arxiv:2111.12682."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3332466.3374503"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 205\u2013217","author":"Krebbers Robbert","year":"2017","unstructured":"Robbert Krebbers , Amin Timany , and Lars Birkedal . 2017 . Interactive Proofs in Higher-Order Concurrent Separation Logic . In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 205\u2013217 . Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive Proofs in Higher-Order Concurrent Separation Logic. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 205\u2013217."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386029"},{"key":"e_1_2_1_29_1","unstructured":"Morten Krogh-Jespersen Thomas Dinsdale-Young and Lars Birkedal. 2016. Verifying a concurrent data-structure from the Dartino Framework in Iris. \t\t\t\t  Morten Krogh-Jespersen Thomas Dinsdale-Young and Lars Birkedal. 2016. Verifying a concurrent data-structure from the Dartino Framework in Iris."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.03.007"},{"key":"e_1_2_1_31_1","volume-title":"Fast Local-Spin Abortable Mutual Exclusion with Bounded Space. In International Conference On Principles Of Distributed Systems. 364\u2013379","author":"Lee Hyonho","year":"2010","unstructured":"Hyonho Lee . 2010 . Fast Local-Spin Abortable Mutual Exclusion with Bounded Space. In International Conference On Principles Of Distributed Systems. 364\u2013379 . Hyonho Lee. 2010. Fast Local-Spin Abortable Mutual Exclusion with Bounded Space. In International Conference On Principles Of Distributed Systems. 364\u2013379."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2004.8"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/645604.662740"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2442516.2442527"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the 36th International Conference on Software Engineering. 1117\u20131127","author":"Okur Semih","year":"2014","unstructured":"Semih Okur , David L Hartveld , Danny Dig , and Arie van Deursen . 2014 . A Study and Toolkit for Asynchronous Programming in C# . In Proceedings of the 36th International Conference on Software Engineering. 1117\u20131127 . Semih Okur, David L Hartveld, Danny Dig, and Arie van Deursen. 2014. A Study and Toolkit for Asynchronous Programming in C#. In Proceedings of the 36th International Conference on Software Engineering. 1117\u20131127."},{"key":"e_1_2_1_38_1","volume-title":"RMR-Efficient Randomized Abortable Mutual Exclusion. In International Symposium on Distributed Computing. 267\u2013281","author":"Pareek Abhijeet","year":"2012","unstructured":"Abhijeet Pareek and Philipp Woelfel . 2012 . RMR-Efficient Randomized Abortable Mutual Exclusion. In International Symposium on Distributed Computing. 267\u2013281 . Abhijeet Pareek and Philipp Woelfel. 2012. RMR-Efficient Randomized Abortable Mutual Exclusion. In International Symposium on Distributed Computing. 267\u2013281."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2018.3"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087556.3087588"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming. 147\u2013156","author":"William N","year":"2006","unstructured":"William N Scherer III, Doug Lea , and Michael L Scott . 2006 . Scalable Synchronous Queues . In Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming. 147\u2013156 . William N Scherer III, Doug Lea, and Michael L Scott. 2006. Scalable Synchronous Queues. In Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming. 147\u2013156."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_2_1_43_1","volume-title":"Folly Library. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. 100\u2013115","author":"Vindum Simon Friis","year":"2022","unstructured":"Simon Friis Vindum , Dan Frumin , and Lars Birkedal . 2022 . Mechanized Verification of a Fine-Grained Concurrent Queue from Meta\u2019s Folly Library. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. 100\u2013115 . Simon Friis Vindum, Dan Frumin, and Lars Birkedal. 2022. Mechanized Verification of a Fine-Grained Concurrent Queue from Meta\u2019s Folly Library. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. 100\u2013115."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3016078.2851168"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591230","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591230","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:46Z","timestamp":1750178866000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591230"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":44,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591230"],"URL":"https:\/\/doi.org\/10.1145\/3591230","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}