{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T05:00:15Z","timestamp":1790658015624,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":99,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,9,28]],"date-time":"2026-09-28T00:00:00Z","timestamp":1790553600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,9,29]]},"DOI":"10.1145\/3830418.3843879","type":"proceedings-article","created":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T03:52:13Z","timestamp":1790653933000},"page":"636-655","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Lion: Modular Verification of Async Runtime Liveness"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2871-3785","authenticated-orcid":false,"given":"Ti","family":"Zhou","sequence":"first","affiliation":[{"name":"Stony Brook University, Stony Brook, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-3138-3901","authenticated-orcid":false,"given":"Zihao","family":"Zhang","sequence":"additional","affiliation":[{"name":"Stony Brook University, Stony Brook, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1356-6279","authenticated-orcid":false,"given":"Omar","family":"Chowdhury","sequence":"additional","affiliation":[{"name":"Stony Brook University, Stony Brook, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8244-2109","authenticated-orcid":false,"given":"Shuai","family":"Mu","sequence":"additional","affiliation":[{"name":"Stony Brook University, Stony Brook, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,9,28]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Abhashkumar Anubhavnidhi","year":"2020","unstructured":"Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. Tiramisu: Fast multilayer network verification. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2020."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_3_2_1_3_1","volume-title":"Efficient IO with io_uring. https:\/\/web.archive.org\/web\/20260624135046\/https:\/\/kernel.dk\/io_uring.pdf","author":"Axboe Jens","year":"2019","unstructured":"Jens Axboe. Efficient IO with io_uring. https:\/\/web.archive.org\/web\/20260624135046\/https:\/\/kernel.dk\/io_uring.pdf, 2019."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_3_2_1_5_1","volume-title":"rumqtt: MQTT client and broker in Rust. https:\/\/github.com\/bytebeamio\/rumqtt. Accessed","year":"2026","unstructured":"Bytebeam. rumqtt: MQTT client and broker in Rust. https:\/\/github.com\/bytebeamio\/rumqtt. Accessed 2026."},{"key":"e_1_3_2_1_6_1","volume-title":"Monoio - a thread-per-core Rust async runtime based on io_uring. Accessed","year":"2026","unstructured":"ByteDance. Monoio - a thread-per-core Rust async runtime based on io_uring. Accessed 2026."},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Chajed Tej","year":"2018","unstructured":"Tej Chajed, M. Frans Kaashoek, Butler W. Lampson, and Nickolai Zeldovich. Verifying concurrent software using movers in CSPEC. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2018."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314585"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Chajed Tej","year":"2021","unstructured":"Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, and Nickolai Zeldovich. GoJournal: A verified, concurrent, crash-safe journaling system. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2021."},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Chajed Tej","year":"2022","unstructured":"Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2022."},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Chang Yun-Sheng","year":"2023","unstructured":"Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying vMVCC, a high-performance transaction library using multi-version concurrency control. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2023."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3625275.3625401"},{"key":"e_1_3_2_1_16_1","volume-title":"Pingora: A library for building fast, reliable and evolvable network services. https:\/\/github.com\/cloudflare\/pingora. Accessed","year":"2026","unstructured":"Cloudflare. Pingora: A library for building fast, reliable and evolvable network services. https:\/\/github.com\/cloudflare\/pingora. Accessed 2026."},{"key":"e_1_3_2_1_17_1","volume-title":"Glommio - a thread-per-core crate for Rust and Linux. Accessed","author":"Costa Glauber","year":"2026","unstructured":"Glauber Costa and Datadog. Glommio - a thread-per-core crate for Rust and Linux. Accessed 2026."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180199"},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2016."},{"key":"e_1_3_2_1_22_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Hance Travis","year":"2021","unstructured":"Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. Finding invariants of distributed systems: It's a small (enough) world after all. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2021."},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Hance Travis","year":"2020","unstructured":"Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. Storage systems are distributed systems (so verify them that way!). In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2020."},{"key":"e_1_3_2_1_24_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Hance Travis","year":"2023","unstructured":"Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno. Sharding the state machine: Automated modular reasoning for complex concurrent systems. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2023."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Ileri Atalay Mert","year":"2018","unstructured":"Atalay Mert Ileri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Proving confidentiality in a file system using DiskSec. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2018."},{"key":"e_1_3_2_1_27_1","unstructured":"Hans Kamp. Tense Logic and the Theory of Linear Order. PhD thesis University of California Los Angeles 1968."},{"key":"e_1_3_2_1_28_1","unstructured":"Dan Kegel. The C10K problem. http:\/\/www.kegel.com\/c10k.html 1999. Accessed 2026."},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Killian Charles","year":"2007","unstructured":"Charles Killian, James W. Anderson, Ranjit Jhala, and Amin Vahdat. Life, death, and the critical transition: Finding liveness bugs in systems code. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2007."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_14"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_33_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695952"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_1_36_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"LeBlanc Hayley","year":"2025","unstructured":"Hayley LeBlanc, Jacob R. Lorch, Chris Hawblitzel, Cheng Huang, Yiheng Tao, Nickolai Zeldovich, and Vijay Chidambaram. PoWER never corrupts: Tool-agnostic verification of crash consistency and corruption detection. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2025."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_38_1","volume-title":"Formal verification of a realistic compiler. Communications of the ACM, 52(7)","author":"Leroy Xavier","year":"2009","unstructured":"Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7), 2009."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_3_2_1_40_1","volume-title":"Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP)","author":"Li Jing","year":"2016","unstructured":"Jing Li, Kunal Agrawal, Sameh Elnikety, Yuxiong He, I-Ting Angelina Lee, Chenyang Lu, and Kathryn S. McKinley. Work stealing for interactive services to meet target latency. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), 2016."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00049"},{"key":"e_1_3_2_1_42_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Li Xupeng","year":"2022","unstructured":"Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, and Gareth Stockwell. Design and verification of the Arm confidential compute architecture. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2022."},{"key":"e_1_3_2_1_43_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Li Xupeng","year":"2023","unstructured":"Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh. Spoq: Scaling machine-checkable systems verification in Coq. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2023."},{"key":"e_1_3_2_1_44_1","volume-title":"evhttp: Fix failure to send all output data for POST\/PUT requests","author":"PR","year":"2015","unstructured":"libevent contributors. PR #190: evhttp: Fix failure to send all output data for POST\/PUT requests, 2015."},{"key":"e_1_3_2_1_45_1","volume-title":"libuv - multi-platform support library with a focus on asynchronous I\/O. Accessed","year":"2026","unstructured":"libuv contributors. libuv - multi-platform support library with a focus on asynchronous I\/O. Accessed 2026."},{"key":"e_1_3_2_1_46_1","volume-title":"Proceedings of the USENIX Annual Technical Conference (ATC)","author":"Ma Haojun","year":"2022","unstructured":"Haojun Ma, Hammad Ahmad, Aman Goel, Eli Goldweber, Jean-Baptiste Jeannin, Manos Kapritsos, and Baris Kasikci. Sift: Using refinement-guided automation to verify complex distributed systems. In Proceedings of the USENIX Annual Technical Conference (ATC), 2022."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_49_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Nelson Luke","year":"2017","unstructured":"Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-button verification of an OS kernel. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2017."},{"key":"e_1_3_2_1_50_1","volume-title":"How Amazon Web Services uses formal methods. Communications of the ACM, 58(4)","author":"Newcombe Chris","year":"2015","unstructured":"Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. How Amazon Web Services uses formal methods. Communications of the ACM, 58(4), 2015."},{"key":"e_1_3_2_1_51_1","volume-title":"Issue #8334: Large number of stored certificates correlated with hanging API requests","author":"Company Oxide Computer","year":"2025","unstructured":"Oxide Computer Company. Issue #8334: Large number of stored certificates correlated with hanging API requests, 2025."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158114"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_1_54_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Pirelli Solal","year":"2022","unstructured":"Solal Pirelli, Akvil\u0117 Valentukonyt\u0117, Katerina J. Argyraki, and George Candea. Automated verification of network function binaries. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2022."},{"key":"e_1_3_2_1_55_1","volume-title":"libevent - an event notification library. Accessed","author":"Provos Niels","year":"2026","unstructured":"Niels Provos and Nick Mathewson. libevent - an event notification library. Accessed 2026."},{"key":"e_1_3_2_1_56_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Ryzhyk Leonid","year":"2017","unstructured":"Leonid Ryzhyk, Nikolaj S. Bj\u00f8rner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry, and George Varghese. Correct by construction networks using stepwise refinement. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2017."},{"key":"e_1_3_2_1_57_1","volume-title":"Seastar - high-performance server-side application framework. Accessed","author":"DB.","year":"2026","unstructured":"ScyllaDB. Seastar - high-performance server-side application framework. Accessed 2026."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_3_2_1_60_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-button verification of file systems via crash refinement. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2016."},{"key":"e_1_3_2_1_61_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sigurbjarnarson Helgi","year":"2018","unstructured":"Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. Nickel: A framework for design and verification of information flow control systems. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2018."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428220"},{"key":"e_1_3_2_1_63_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sun Xudong","year":"2024","unstructured":"Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. Anvil: Verifying liveness of cluster management controllers. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2024."},{"key":"e_1_3_2_1_64_1","volume-title":"Proceedings of the USENIX Annual Technical Conference (ATC)","author":"Tang Ruize","year":"2025","unstructured":"Ruize Tang, Minghua Wang, Xudong Sun, Lin Huang, Yu Huang, and Xiaoxing Ma. Converos: Practical model checking for verifying Rust OS kernel concurrency. In Proceedings of the USENIX Annual Technical Conference (ATC), 2025."},{"key":"e_1_3_2_1_65_1","volume-title":"axum: Ergonomic and modular web framework built with Tokio, Tower, and Hyper. https:\/\/github.com\/tokio-rs\/axum. Accessed","author":"Tokio","year":"2026","unstructured":"Tokio contributors. axum: Ergonomic and modular web framework built with Tokio, Tower, and Hyper. https:\/\/github.com\/tokio-rs\/axum. Accessed 2026."},{"key":"e_1_3_2_1_66_1","volume-title":"Tokio - an asynchronous runtime for Rust. Accessed","author":"Tokio","year":"2026","unstructured":"Tokio contributors. Tokio - an asynchronous runtime for Rust. Accessed 2026."},{"key":"e_1_3_2_1_67_1","volume-title":"Tokio API documentation: Blocking and Yielding. Accessed","author":"Tokio","year":"2026","unstructured":"Tokio contributors. Tokio API documentation: Blocking and Yielding. Accessed 2026."},{"key":"e_1_3_2_1_68_1","volume-title":"Issue #703: Weird non-blocking block when using two nested tokio::spawn statements","author":"Tokio","year":"2018","unstructured":"Tokio contributors. Issue #703: Weird non-blocking block when using two nested tokio::spawn statements, 2018."},{"key":"e_1_3_2_1_69_1","volume-title":"Issue #1092: Memory leak","author":"Tokio","year":"2019","unstructured":"Tokio contributors. Issue #1092: Memory leak, 2019."},{"key":"e_1_3_2_1_70_1","volume-title":"Issue #3069: Tokio 0.3 timer will hang when duration is small","author":"Tokio","year":"2020","unstructured":"Tokio contributors. Issue #3069: Tokio 0.3 timer will hang when duration is small, 2020."},{"key":"e_1_3_2_1_71_1","volume-title":"Fix readiness future eagerly consuming entire socket readiness","author":"Tokio","year":"2020","unstructured":"Tokio contributors. PR #2887: Fix readiness future eagerly consuming entire socket readiness, 2020."},{"key":"e_1_3_2_1_72_1","volume-title":"time: use intrusive lists for timer tracking","author":"Tokio","year":"2020","unstructured":"Tokio contributors. PR #3080: time: use intrusive lists for timer tracking, 2020."},{"key":"e_1_3_2_1_73_1","volume-title":"Issue #4941: rt: make the LIFO slot in the multithreaded scheduler stealable","author":"Tokio","year":"2022","unstructured":"Tokio contributors. Issue #4941: rt: make the LIFO slot in the multithreaded scheduler stealable, 2022."},{"key":"e_1_3_2_1_74_1","volume-title":"Issue #5020: LocalEnterGuard would cause current thread runtime to become stuck","author":"Tokio","year":"2022","unstructured":"Tokio contributors. Issue #5020: LocalEnterGuard would cause current thread runtime to become stuck, 2022."},{"key":"e_1_3_2_1_75_1","volume-title":"Issue #5894: Sleep is not firing when macOS goes to sleep and then awakens","author":"Tokio","year":"2023","unstructured":"Tokio contributors. Issue #5894: Sleep is not firing when macOS goes to sleep and then awakens, 2023."},{"key":"e_1_3_2_1_76_1","volume-title":"tokio: distinguish LocalSet::enter() with being polled","author":"Tokio","year":"2023","unstructured":"Tokio contributors. PR #6016: tokio: distinguish LocalSet::enter() with being polled, 2023."},{"key":"e_1_3_2_1_77_1","volume-title":"io: fix possible I\/O resource hang","author":"Tokio","year":"2023","unstructured":"Tokio contributors. PR #6134: io: fix possible I\/O resource hang, 2023."},{"key":"e_1_3_2_1_78_1","volume-title":"Issue #6315: rt: Tolerate slow task polls","author":"Tokio","year":"2024","unstructured":"Tokio contributors. Issue #6315: rt: Tolerate slow task polls, 2024."},{"key":"e_1_3_2_1_79_1","volume-title":"Using sharded locks instead of a global lock for timers","author":"Tokio","year":"2024","unstructured":"Tokio contributors. PR #6534: Using sharded locks instead of a global lock for timers, 2024."},{"key":"e_1_3_2_1_80_1","volume-title":"time: update wake_up while holding all the locks of sharded time wheels","author":"Tokio","year":"2024","unstructured":"Tokio contributors. PR #6683: time: update wake_up while holding all the locks of sharded time wheels, 2024."},{"key":"e_1_3_2_1_81_1","volume-title":"Issue #7210: yield_now should not defer inside block_in_place","author":"Tokio","year":"2025","unstructured":"Tokio contributors. Issue #7210: yield_now should not defer inside block_in_place, 2025."},{"key":"e_1_3_2_1_82_1","volume-title":"Issue #7478: [bug] handle.dump() causes multi_thread issues (partially working or all sleeping)","author":"Tokio","year":"2025","unstructured":"Tokio contributors. Issue #7478: [bug] handle.dump() causes multi_thread issues (partially working or all sleeping), 2025."},{"key":"e_1_3_2_1_83_1","volume-title":"rt: skip defer queue in block_in_place context","author":"Tokio","year":"2025","unstructured":"Tokio contributors. PR #7216: rt: skip defer queue in block_in_place context, 2025."},{"key":"e_1_3_2_1_84_1","volume-title":"Issue #8198: alternative timer compatibility hazard","author":"Tokio","year":"2026","unstructured":"Tokio contributors. Issue #8198: alternative timer compatibility hazard, 2026."},{"key":"e_1_3_2_1_85_1","volume-title":"tokio-util: wake DelayQueue when cleared","author":"Tokio","year":"2026","unstructured":"Tokio contributors. PR #8320: tokio-util: wake DelayQueue when cleared, 2026."},{"key":"e_1_3_2_1_86_1","volume-title":"rt: preserve the full ScheduledIo tick in readiness events","author":"Tokio","year":"2026","unstructured":"Tokio contributors. PR #8331: rt: preserve the full ScheduledIo tick in readiness events, 2026."},{"key":"e_1_3_2_1_87_1","volume-title":"Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)","author":"v. Gleissenthall Klaus","year":"2019","unstructured":"Klaus v. Gleissenthall, Rami G\u00f6khan K\u0131c\u0131, Alexander Bakst, Deian Stefan, and Ranjit Jhala. Pretend synchrony: Synchronous verification of asynchronous distributed programs. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2019."},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_89_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Yao Jianan","year":"2022","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. DuoAI: Fast, automated inference of inductive invariants for verifying distributed protocols. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2022."},{"key":"e_1_3_2_1_90_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Yao Jianan","year":"2021","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. DistAI: Data-driven automated invariant learning for distributed protocols. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2021."},{"key":"e_1_3_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/3731569.3764836"},{"key":"e_1_3_2_1_92_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Zhang Kaiyuan","year":"2020","unstructured":"Kaiyuan Zhang, Danyang Zhuo, Aditya Akella, Arvind Krishnamurthy, and Xi Wang. Automated verification of customizable middlebox properties with Gravel. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2020."},{"key":"e_1_3_2_1_93_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zhang Tony Nuda","year":"2024","unstructured":"Tony Nuda Zhang, Travis Hance, Manos Kapritsos, Tej Chajed, and Bryan Parno. Inductive invariants that spark joy: Using invariant taxonomies to streamline distributed protocol proofs. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2024."},{"key":"e_1_3_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591235"},{"key":"e_1_3_2_1_95_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zhang Tony Nuda","year":"2025","unstructured":"Tony Nuda Zhang, Keshav Singh, Tej Chajed, Manos Kapritsos, and Bryan Parno. Basilisk: Using provenance invariants to automate proofs of undecidable protocols. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2025."},{"key":"e_1_3_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/3731569.3764822"},{"key":"e_1_3_2_1_97_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zhou Ziqiao","year":"2024","unstructured":"Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, and Weidong Cui. VeriSMo: A verified security module for confidential VMs. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2024."},{"key":"e_1_3_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359644"},{"key":"e_1_3_2_1_99_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zou Mo","year":"2024","unstructured":"Mo Zou, Dong Du, Mingkai Dong, and Haibo Chen. Using dynamically layered definite releases for verifying the RefFS file system. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2024."}],"event":{"name":"SOSP '26: ACM SIGOPS 32nd Symposium on Operating Systems Principles","location":"Prague Czech Republic","acronym":"SOSP '26","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"]},"container-title":["Proceedings of the ACM SIGOPS 32nd Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3830418.3843879","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T04:51:35Z","timestamp":1790657495000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3830418.3843879"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,9,28]]},"references-count":99,"alternative-id":["10.1145\/3830418.3843879","10.1145\/3830418"],"URL":"https:\/\/doi.org\/10.1145\/3830418.3843879","relation":{},"subject":[],"published":{"date-parts":[[2026,9,28]]},"assertion":[{"value":"2026-09-28","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}