{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T05:39:59Z","timestamp":1769751599497,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":90,"publisher":"ACM","funder":[{"DOI":"10.13039\/501100007937","name":"Peking University","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100007937","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Science Foundation of China","award":["2032001"],"award-info":[{"award-number":["2032001"]}]},{"name":"National Science Foundation of China","award":["62032008"],"award-info":[{"award-number":["62032008"]}]},{"name":"National Science Foundation of China","award":["6237201"],"award-info":[{"award-number":["6237201"]}]},{"name":"AntGroup"},{"name":"National Key R&D Program of China","award":["2022YFB4500701"],"award-info":[{"award-number":["2022YFB4500701"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3731569.3764836","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:43:24Z","timestamp":1759322604000},"page":"1082-1098","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["CortenMM: Efficient Memory Management with Strong Correctness Guarantees"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9268-6278","authenticated-orcid":false,"given":"Junyang","family":"Zhang","sequence":"first","affiliation":[{"name":"National Key Laboratory for Multimedia Information Processing, School of Computer Science, Peking University, Beijing, China"},{"name":"Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-2175-0750","authenticated-orcid":false,"given":"Xiangcan","family":"Xu","sequence":"additional","affiliation":[{"name":"National Key Laboratory for Multimedia Information Processing, School of Computer Science, Peking University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5978-8934","authenticated-orcid":false,"given":"Yonghao","family":"Zou","sequence":"additional","affiliation":[{"name":"National Key Laboratory for Multimedia Information Processing, School of Computer Science, Peking University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-0449-6581","authenticated-orcid":false,"given":"Zhe","family":"Tang","sequence":"additional","affiliation":[{"name":"National Key Laboratory for Multimedia Information Processing, School of Computer Science, Peking University, Beijing, China"},{"name":"Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-3543-499X","authenticated-orcid":false,"given":"Xinyi","family":"Wan","sequence":"additional","affiliation":[{"name":"Ant Group, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5256-2863","authenticated-orcid":false,"given":"Kang","family":"Hu","sequence":"additional","affiliation":[{"name":"National Key Laboratory for Multimedia Information Processing, School of Computer Science, Peking University, Beijing, China"},{"name":"Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-9901-0279","authenticated-orcid":false,"given":"Siyuan","family":"Wang","sequence":"additional","affiliation":[{"name":"National Key Laboratory for Multimedia Information Processing, School of Computer Science, Peking University, Beijing, China"},{"name":"Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5563-7701","authenticated-orcid":false,"given":"Wenbo","family":"Xu","sequence":"additional","affiliation":[{"name":"Key Laboratory of High Confidence Software Technologies (Peking University), Ministry of Education; School of Computer Science, Peking University, Beijing, China"},{"name":"Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2418-7987","authenticated-orcid":false,"given":"Di","family":"Wang","sequence":"additional","affiliation":[{"name":"Key Laboratory of High Confidence Software Technologies (Peking University), Ministry of Education; School of Computer Science, Peking University, Beijing, China"},{"name":"Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1180-9433","authenticated-orcid":false,"given":"Hao","family":"Chen","sequence":"additional","affiliation":[{"name":"CertiK, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-5659-1471","authenticated-orcid":false,"given":"Lin","family":"Huang","sequence":"additional","affiliation":[{"name":"Ant Group, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-9580-5395","authenticated-orcid":false,"given":"Shoumeng","family":"Yan","sequence":"additional","affiliation":[{"name":"Ant Group, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-1266-4815","authenticated-orcid":false,"given":"Yuval","family":"Tamir","sequence":"additional","affiliation":[{"name":"UCLA, Los Angeles, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7903-0717","authenticated-orcid":false,"given":"Yingwei","family":"Luo","sequence":"additional","affiliation":[{"name":"National Key Laboratory for Multimedia Information Processing, School of Computer Science, Peking University, Beijing, China"},{"name":"Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6951-1613","authenticated-orcid":false,"given":"Xiaolin","family":"Wang","sequence":"additional","affiliation":[{"name":"National Key Laboratory for Multimedia Information Processing, School of Computer Science, Peking University, Beijing, China"},{"name":"Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-0642-6006","authenticated-orcid":false,"given":"Huashan","family":"Yu","sequence":"additional","affiliation":[{"name":"National Key Laboratory for Multimedia Information Processing, School of Computer Science, Peking University, Beijing, China"},{"name":"Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0429-4371","authenticated-orcid":false,"given":"Zhenlin","family":"Wang","sequence":"additional","affiliation":[{"name":"Michigan Tech, Houghton, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-1248-4078","authenticated-orcid":false,"given":"Hongliang","family":"Tian","sequence":"additional","affiliation":[{"name":"Ant Group, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-8620-1064","authenticated-orcid":false,"given":"Diyu","family":"Zhou","sequence":"additional","affiliation":[{"name":"National Key Laboratory for Multimedia Information Processing, School of Computer Science, Peking University, Beijing, China"}]}],"member":"320","published-online":{"date-parts":[[2025,10,12]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"What is RCU Fundamentally? 2007. https:\/\/lwn.net\/Articles\/262464\/."},{"key":"e_1_3_2_1_2_1","unstructured":"CVE-2023-3269 2023. https:\/\/www.cve.org\/CVERecord?id=CVE-2023-3269."},{"key":"e_1_3_2_1_3_1","unstructured":"CVE-2023-4611 2023. https:\/\/www.cve.org\/CVERecord?id=CVE-2023-4611."},{"key":"e_1_3_2_1_4_1","unstructured":"CVE-2024-1312 2024. https:\/\/www.cve.org\/CVERecord?id=CVE-2024-1312."},{"key":"e_1_3_2_1_5_1","unstructured":"CVE-2024-27022 2024. https:\/\/www.cve.org\/CVERecord?id=CVE-2024-27022."},{"key":"e_1_3_2_1_6_1","unstructured":"CVE-2024-47676 2024. https:\/\/www.cve.org\/CVERecord?id=CVE-2024-47676."},{"key":"e_1_3_2_1_7_1","unstructured":"CVE-2024-50066 2024. https:\/\/www.cve.org\/CVERecord?id=CVE-2024-50066."},{"key":"e_1_3_2_1_8_1","unstructured":"CVE-2024-56765 2024. https:\/\/www.cve.org\/CVERecord?id=CVE-2024-56765."},{"key":"e_1_3_2_1_9_1","unstructured":"FreeBSD 2024. https:\/\/www.freebsd.org."},{"key":"e_1_3_2_1_10_1","unstructured":"Fuchsia 2024. https:\/\/fuchsia.dev."},{"key":"e_1_3_2_1_11_1","unstructured":"Intel Trust Domain Extensions (Intel TDX) 2024. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/tools\/trust-domain-extensions\/overview.html."},{"key":"e_1_3_2_1_12_1","unstructured":"Linux 2024. https:\/\/www.kernel.org."},{"key":"e_1_3_2_1_13_1","volume-title":"A Unix-like General-Purpose Microkernel-Based Operating System","author":"Redox","year":"2024","unstructured":"Redox: A Unix-like General-Purpose Microkernel-Based Operating System, 2024. https:\/\/www.redox-os.org\/."},{"key":"e_1_3_2_1_14_1","unstructured":"Rust 2024. https:\/\/www.rust-lang.org\/."},{"key":"e_1_3_2_1_15_1","unstructured":"Solaris 2024. https:\/\/www.oracle.com\/solaris\/solaris11."},{"key":"e_1_3_2_1_16_1","unstructured":"Windows 2024. https:\/\/www.microsoft.com\/en-us\/windows."},{"key":"e_1_3_2_1_17_1","unstructured":"ARM 2025. https:\/\/www.arm.com."},{"key":"e_1_3_2_1_18_1","unstructured":"CVE-2025-21696 2025. https:\/\/www.cve.org\/CVERecord?id=CVE-2025-21696."},{"key":"e_1_3_2_1_19_1","unstructured":"CVE-2025-21932 2025. https:\/\/www.cve.org\/CVERecord?id=CVE-2025-21932."},{"key":"e_1_3_2_1_20_1","unstructured":"CVE-2025-21984 2025. https:\/\/www.cve.org\/CVERecord?id=CVE-2025-21984."},{"key":"e_1_3_2_1_21_1","unstructured":"Intel 64 and IA-32 Architectures Software Developer's Manual 2025. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/intel-sdm.html."},{"key":"e_1_3_2_1_22_1","unstructured":"RISC-V 2025. https:\/\/riscv.org."},{"key":"e_1_3_2_1_23_1","unstructured":"Tracking issue for specialization (RFC 1210) 2025. https:\/\/github.com\/rust-lang\/rust\/issues\/31844."},{"key":"e_1_3_2_1_24_1","unstructured":"What is the purpose of Break-Before-Make (FEAT_BBM) in the Arm Architecture? 2025. https:\/\/developer.arm.com\/documentation\/ka006181\/latest\/."},{"key":"e_1_3_2_1_25_1","volume-title":"Proceedings of the 15th European Conference on Computer Systems (EuroSys)","author":"Amit Nadav","year":"2020","unstructured":"Nadav Amit, Amy Tai, and Michael Wei. Don't Shoot Down TLB Shoot-downs! In Proceedings of the 15th European Conference on Computer Systems (EuroSys), Heraklion, Greece, April 2020."},{"key":"e_1_3_2_1_26_1","unstructured":"Oracle Corporation and\/or its affiliates. OpenJDK 2025. https:\/\/openjdk.org\/."},{"key":"e_1_3_2_1_27_1","volume-title":"Proceedings of the 2003 USENIX Annual Technical Conference (ATC)","author":"Appavoo Jonathan","year":"2003","unstructured":"Jonathan Appavoo, Marc Auslander, Dilma Da Silva, David Edelsohn, Orran Krieger, Michal Ostrowski, Bryan Rosenburg, Robert W. Wisniewski, and Jimi Xenidis. Providing a Linux API on the Scalable K42 Kernel. In Proceedings of the 2003 USENIX Annual Technical Conference (ATC), San Antonio, TX, June 2003."},{"key":"e_1_3_2_1_28_1","volume-title":"Operating Systems: Three Easy Pieces","author":"Arpaci-Dusseau Remzi H","year":"2018","unstructured":"Remzi H Arpaci-Dusseau and Andrea C Arpaci-Dusseau. Operating Systems: Three Easy Pieces. 2018."},{"key":"e_1_3_2_1_29_1","unstructured":"Suren Baghdasaryan. [PATCH v3 00\/35] Per-VMA Locks 2023. https:\/\/lore.kernel.org\/lkml\/ZCstwjKhn76%2FmxIa@casper.infradead.org\/t\/."},{"key":"e_1_3_2_1_30_1","unstructured":"Suren Baghdasaryan. Per-VMA Locks 2023. https:\/\/lwn.net\/Articles\/924572\/."},{"key":"e_1_3_2_1_31_1","volume-title":"Akhilesh Singhania. The Multikernel: A New OS Architecture for Scalable Multicore Systems. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP)","author":"Baumann Andrew","year":"2009","unstructured":"Andrew Baumann, Paul Barham, Pierre-Evariste Dagand, Tim Harris, Rebecca Isaacs, Simon Peter, Timothy Roscoe, Adrian Sch\u00fcpbach, and Akhilesh Singhania. The Multikernel: A New OS Architecture for Scalable Multicore Systems. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), Big Sky, MT, October 2009."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/12518"},{"key":"e_1_3_2_1_33_1","first-page":"312","volume-title":"Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Bhardwaj Ankit","year":"2021","unstructured":"Ankit Bhardwaj, Chinmay Kulkarni, Reto Achermann, Irina Calciu, Sanidhya Kashyap, Ryan Stutsman, Amy Tai, and Gerd Zellweger. NrOS: Effective Replication and Sharing in an Operating System. In Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 295\u2013312, Virtual, July 2021."},{"key":"e_1_3_2_1_34_1","volume-title":"Benchmarking Modern Multiprocessors","author":"Bienia Christian","year":"2011","unstructured":"Christian Bienia. Benchmarking Modern Multiprocessors. Princeton University, 2011."},{"key":"e_1_3_2_1_35_1","volume-title":"Lin Zhong. Theseus: An Experiment in Operating System Structure and State Management. In Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Boos Kevin","year":"2020","unstructured":"Kevin Boos, Namitha Liyanage, Ramla Ijaz, and Lin Zhong. Theseus: An Experiment in Operating System Structure and State Management. In Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Banff, Canada, November 2020."},{"key":"e_1_3_2_1_36_1","volume-title":"Proceedings of the 9th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Boyd-Wickizer Silas","year":"2010","unstructured":"Silas Boyd-Wickizer, Austin T. Clements, Yandong Mao, Aleksey Pesterev, M. Frans Kaashoek, Robert Morris, and Nickolai Zeldovich. An Analysis of Linux Scalability to Many Cores. In Proceedings of the 9th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Vancouver, Canada, October 2010."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-010-9097-2"},{"key":"e_1_3_2_1_38_1","first-page":"165","volume-title":"19th USENIX Workshop on Hot Topics in Operating Systems (HotOS) (HotOS XIX)","author":"Brun Matthias","year":"2023","unstructured":"Matthias Brun, Reto Achermann, Tej Chajed, Jon Howell, Gerd Zellweger, and Andrea Lattuada. Beyond Isolation: OS Verification as a Foundation for Correct Applications. In 19th USENIX Workshop on Hot Topics in Operating Systems (HotOS) (HotOS XIX), pages 158\u2013165, Providence, RI, June 2023."},{"key":"e_1_3_2_1_39_1","first-page":"221","volume-title":"Proceedings of the 22nd ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Calciu Irina","year":"2017","unstructured":"Irina Calciu, Siddhartha Sen, Mahesh Balakrishnan, and Marcos K. Aguilera. Black-box Concurrent Data Structures for NUMA Architectures. In Proceedings of the 22nd ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 207\u2013221, Xi'an, China, April 2017."},{"key":"e_1_3_2_1_40_1","first-page":"485","volume-title":"Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Chen Haibo","year":"2024","unstructured":"Haibo Chen, Xie Miao, Ning Jia, Nan Wang, Yu Li, Nian Liu, Yutao Liu, Fei Wang, Qiang Huang, Kun Li, et al. Microkernel Goes General: Performance and Compatibility in the HongMeng Production Microkernel. In Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 465\u2013485, Santa Clara, CA, July 2024."},{"key":"e_1_3_2_1_41_1","first-page":"17","volume-title":"Anton Burtsev. Atmosphere: Towards Practical Verified Kernels in Rust. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification (KISV)","author":"Chen Xiangdong","year":"2023","unstructured":"Xiangdong Chen, Zhaofeng Li, Lukas Mesicek, Vikram Narayanan, and Anton Burtsev. Atmosphere: Towards Practical Verified Kernels in Rust. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification (KISV), pages 9\u201317, Koblenz, Germany, October 2023."},{"key":"e_1_3_2_1_42_1","volume-title":"Proceedings of the 17th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Clements Austin T.","year":"2012","unstructured":"Austin T. Clements, M. Frans Kaashoek, and Nickolai Zeldovich. Scalable Address Spaces Using RCU Balanced Trees. In Proceedings of the 17th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), London, UK, March 2012."},{"key":"e_1_3_2_1_43_1","first-page":"224","volume-title":"Nickolai Zeldovich. RadixVM: Scalable Address Spaces for Multithreaded Applications. In Proceedings of the 8th European Conference on Computer Systems (EuroSys)","author":"Clements Austin T.","year":"2013","unstructured":"Austin T. Clements, M. Frans Kaashoek, and Nickolai Zeldovich. RadixVM: Scalable Address Spaces for Multithreaded Applications. In Proceedings of the 8th European Conference on Computer Systems (EuroSys), pages 211\u2013224, Prague, Czech Republic, April 2013."},{"key":"e_1_3_2_1_44_1","volume-title":"Memory protection keys","author":"Corbet Jonathan","year":"2015","unstructured":"Jonathan Corbet. Memory protection keys, 2015. https:\/\/lwn.net\/Articles\/643797\/."},{"key":"e_1_3_2_1_45_1","volume-title":"The Ongoing Search for mmap_lock Scalability","author":"Corbet Jonathan","year":"2022","unstructured":"Jonathan Corbet. The Ongoing Search for mmap_lock Scalability, 2022. https:\/\/lwn.net\/Articles\/893906\/."},{"key":"e_1_3_2_1_46_1","volume-title":"Stabilizing Per-VMA Locking","author":"Corbet Jonathan","year":"2023","unstructured":"Jonathan Corbet. Stabilizing Per-VMA Locking, 2023. https:\/\/lwn.net\/Articles\/937943\/."},{"key":"e_1_3_2_1_47_1","volume-title":"Linux Device Drivers. \"O'Reilly Media","author":"Corbet Jonathan","year":"2005","unstructured":"Jonathan Corbet, Alessandro Rubini, and Greg Kroah-Hartman. Linux Device Drivers. \"O'Reilly Media, Inc.\", 3 edition, 2005."},{"key":"e_1_3_2_1_48_1","volume-title":"lmbench","author":"Intel Corporation","year":"2025","unstructured":"Intel Corporation. lmbench, 2025. https:\/\/github.com\/intel\/lmbench."},{"key":"e_1_3_2_1_49_1","first-page":"328","volume-title":"Dice and Alex Kogan. BRAVO: Biased Locking for Reader-Writer Locks. In Proceedings of the 2019 USENIX Annual Technical Conference (ATC)","author":"Dave","year":"2019","unstructured":"Dave Dice and Alex Kogan. BRAVO: Biased Locking for Reader-Writer Locks. In Proceedings of the 2019 USENIX Annual Technical Conference (ATC), pages 315\u2013328, Renton, WA, July 2019. USENIX Association."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/360363.360369"},{"key":"e_1_3_2_1_51_1","first-page":"305","volume-title":"Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP)","author":"Ferraiuolo Andrew","year":"2017","unstructured":"Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), pages 287\u2013305, Shanghai, China, October 2017."},{"key":"e_1_3_2_1_52_1","first-page":"94","volume-title":"Proceedings of the USENIX Summer Conference","author":"Gingell Robert A.","unstructured":"Robert A. Gingell, Joseph P. Moran, and William A. Shannon. Virtual Memory Architecture in SunOS. In Proceedings of the USENIX Summer Conference, pages 81\u201394. USENIX Association, 1987."},{"key":"e_1_3_2_1_53_1","first-page":"278","volume-title":"Proceedings of the 2005 USENIX Annual Technical Conference (ATC)","author":"Gray Charles","year":"2005","unstructured":"Charles Gray, Matthew Chapman, Peter Chubb, David Mosberger-Tang, and Gernot Heiser. Itanium\u2014A System Implementor's Tale. In Proceedings of the 2005 USENIX Annual Technical Conference (ATC), pages 264\u2013278, Anaheim, CA, April 2005."},{"key":"e_1_3_2_1_54_1","first-page":"669","volume-title":"David Costanzo. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th 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 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 653\u2013669, Savannah, GA, November 2016."},{"key":"e_1_3_2_1_55_1","unstructured":"Liam R. Howlett. Maple Tree 2024. https:\/\/docs.kernel.org\/core-api\/maple_tree.html."},{"key":"e_1_3_2_1_56_1","first-page":"50","volume-title":"Huck and Jim Hays. Architectural Support for Translation Table Management in Large Address Space Machines. In Proceedings of the 20th ACM\/IEEE International Symposium on Computer Architecture (ISCA)","author":"Jerry","unstructured":"Jerry Huck and Jim Hays. Architectural Support for Translation Table Management in Large Address Space Machines. In Proceedings of the 20th ACM\/IEEE International Symposium on Computer Architecture (ISCA), pages 39\u201350."},{"key":"e_1_3_2_1_57_1","first-page":"8","volume-title":"Lin Zhong. Leveraging Rust for Lightweight OS Correctness. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification (KISV)","author":"Ijaz Ramla","year":"2023","unstructured":"Ramla Ijaz, Kevin Boos, and Lin Zhong. Leveraging Rust for Lightweight OS Correctness. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification (KISV), pages 1\u20138, Koblenz, Germany, October 2023."},{"key":"e_1_3_2_1_58_1","first-page":"306","volume-title":"Proceedings of the 8th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Bruce","year":"1998","unstructured":"Bruce L. Jacob and Trevor N. Mudge. A look at several memory management units, tlb-refill mechanisms, and page table organizations. In Proceedings of the 8th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 295\u2013306, San Jose, CA, October 1998."},{"key":"e_1_3_2_1_59_1","first-page":"454","volume-title":"Zhengyu He. HyperEnclave: An Open and Cross-platform Trusted Execution Environment. In Proceedings of the 2022 USENIX Annual Technical Conference (ATC)","author":"Jia Yuekai","year":"2022","unstructured":"Yuekai Jia, Shuang Liu, Wenhao Wang, Yu Chen, Zhengde Zhai, Shoumeng Yan, and Zhengyu He. HyperEnclave: An Open and Cross-platform Trusted Execution Environment. In Proceedings of the 2022 USENIX Annual Technical Conference (ATC), pages 437\u2013454, Carlsbad, CA, July 2022."},{"key":"e_1_3_2_1_60_1","volume-title":"Optimizing MapReduce for Multicore Architectures","author":"Kaashoek Frans","year":"2010","unstructured":"Frans Kaashoek, Robert Morris, and Yandong Mao. Optimizing MapReduce for Multicore Architectures. 2010."},{"key":"e_1_3_2_1_61_1","volume-title":"Page Table Isolation (PTI)","author":"The","year":"2025","unstructured":"The kernel development community. Page Table Isolation (PTI), 2025. https:\/\/www.kernel.org\/doc\/html\/next\/x86\/pti.html."},{"key":"e_1_3_2_1_62_1","volume-title":"Process Addresses","author":"The","year":"2025","unstructured":"The kernel development community. Process Addresses, 2025. https:\/\/docs.kernel.org\/mm\/process_addrs.html."},{"key":"e_1_3_2_1_63_1","first-page":"220","volume-title":"Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP)","author":"Klein Gerwin","year":"2009","unstructured":"Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal Verification of an OS Kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), pages 207\u2013220, Big Sky, MT, October 2009."},{"key":"e_1_3_2_1_64_1","first-page":"15","volume-title":"Shady Issa. Scalable Range Locks for Scalable Address Spaces and Beyond. In Proceedings of the 15th European Conference on Computer Systems (EuroSys)","author":"Kogan Alex","year":"2020","unstructured":"Alex Kogan, Dave Dice, and Shady Issa. Scalable Range Locks for Scalable Address Spaces and Beyond. In Proceedings of the 15th European Conference on Computer Systems (EuroSys), pages 1\u201315, Heraklion, Greece, April 2020."},{"key":"e_1_3_2_1_65_1","first-page":"145","volume-title":"Michal Ostrowski, Jonathan Appavoo, Maria Butrico, Mark Mergen, Amos Waterland, and Volkmar Uhlig. K42: Building a Complete Operating System.","author":"Krieger Orran","year":"2006","unstructured":"Orran Krieger, Marc Auslander, Bryan Rosenburg, Robert W. Wisniewski, Jimi Xenidis, Dilma Da Silva, Michal Ostrowski, Jonathan Appavoo, Maria Butrico, Mark Mergen, Amos Waterland, and Volkmar Uhlig. K42: Building a Complete Operating System. pages 133\u2013145, April 2006."},{"key":"e_1_3_2_1_66_1","first-page":"664","volume-title":"Tushar Krishna. LATR: Lazy Translation Coherence. In Proceedings of the 23rd ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Kumar Mohan Kumar","year":"2018","unstructured":"Mohan Kumar Kumar, Steffen Maass, Sanidhya Kashyap, J\u00e1n Vesel\u00fd, Zi Yan, Taesoo Kim, Abhishek Bhattacharjee, and Tushar Krishna. LATR: Lazy Translation Coherence. In Proceedings of the 23rd ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 651\u2013664, Williamsburg, VA, March 2018."},{"key":"e_1_3_2_1_67_1","first-page":"454","volume-title":"Bryan Parno. Verus: A Practical Foundation for Systems Verification. In Proceedings of the 30th ACM Symposium on Operating Systems Principles (SOSP)","author":"Lattuada Andrea","year":"2024","unstructured":"Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno. Verus: A Practical Foundation for Systems Verification. In Proceedings of the 30th ACM Symposium on Operating Systems Principles (SOSP), pages 438\u2013454, Austin, TX, USA, November 2024."},{"key":"e_1_3_2_1_68_1","volume-title":"Proceedings of the 34th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)","author":"Lattuada Andrea","year":"2023","unstructured":"Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust Programs using Linear Ghost Types. In Proceedings of the 34th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Lisbon, Portugal, October 2023."},{"key":"e_1_3_2_1_69_1","first-page":"251","volume-title":"Proceedings of the 26th Symposium on Operating Systems Principles","author":"Levy Amit","year":"2017","unstructured":"Amit Levy, Bradford Campbell, Branden Ghena, Daniel B Giffin, Pat Pannuto, Prabal Dutta, and Philip Levis. Multiprogramming a 64KB Computer Safely and Efficiently. In Proceedings of the 26th Symposium on Operating Systems Principles, pages 234\u2013251, Shanghai, China, October 2017."},{"key":"e_1_3_2_1_70_1","first-page":"44725","article-title":"When Memory Corruption Met Concurrency","volume":"11","author":"Llorente-Vazquez Oscar","year":"2023","unstructured":"Oscar Llorente-Vazquez, Igor Santos-Grueiro, and Pablo Garcia Bringas. When Memory Corruption Met Concurrency: Vulnerabilities in Concurrent Programs. IEEE Access, 11:44725\u201344740, 2023.","journal-title":"Vulnerabilities in Concurrent Programs. IEEE Access"},{"key":"e_1_3_2_1_71_1","volume-title":"Proper Locking Under a Preemptible Kernel: Keeping Kernel Code Preempt-Safe","author":"Love Robert","year":"2025","unstructured":"Robert Love. Proper Locking Under a Preemptible Kernel: Keeping Kernel Code Preempt-Safe, 2025. https:\/\/docs.kernel.org\/locking\/preempt-locking.html."},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.5555\/231070"},{"key":"e_1_3_2_1_73_1","first-page":"294","volume-title":"Proceedings of the 1996 USENIX Annual Technical Conference (ATC)","author":"McVoy Larry","year":"1996","unstructured":"Larry McVoy and Carl Staelin. lmbench: Portable Tools for Performance Analysis. In Proceedings of the 1996 USENIX Annual Technical Conference (ATC), pages 279\u2013294, San Diego, CA, January 1996."},{"issue":"1","key":"e_1_3_2_1_74_1","first-page":"21","volume":"9","author":"Mellor-Crummey John M.","year":"1991","unstructured":"John M. Mellor-Crummey and Michael L. Scott. Algorithms for Scalable Synchronization on Shared-Memory Multiprocessors. ACM Transactions on Computer Systems, 9(1):21\u201365, February 1991.","journal-title":"Scott. Algorithms for Scalable Synchronization on Shared-Memory Multiprocessors. ACM Transactions on Computer Systems"},{"key":"e_1_3_2_1_75_1","volume-title":"VirtualProtect function (memoryapi.h)","year":"2025","unstructured":"Microsoft. VirtualProtect function (memoryapi.h), 2025. https:\/\/learn.microsoft.com\/en-us\/windows\/win32\/api\/memoryapi\/nf-memoryapi-virtualprotect."},{"key":"e_1_3_2_1_76_1","first-page":"39","volume-title":"Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Narayanan Vikram","year":"2020","unstructured":"Vikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel, Zhaofeng Li, Gerd Zellweger, and Anton Burtsev. RedLeaf: Isolation and Communication in a Safe Operating System. In Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 21\u201339, Banff, Canada, November 2020."},{"key":"e_1_3_2_1_77_1","first-page":"269","volume-title":"Proceedings of the 26th 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: PushButton Verification of an OS Kernel. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), pages 252\u2013269, Shanghai, China, October 2017."},{"key":"e_1_3_2_1_78_1","volume-title":"Long-descriptor Format Memory Region Attributes","author":"ARM","year":"2025","unstructured":"ARM Limited (or its affiliates). Long-descriptor Format Memory Region Attributes, 2025. https:\/\/developer.arm.com\/documentation\/ddi0406\/c\/System-Level-Architecture\/Virtual-Memory-System-Architecture-VMSA-\/Memory-region-attributes\/Long-descriptor-format-memory-region-attributes?lang=en."},{"key":"e_1_3_2_1_79_1","volume-title":"Proceedings of the 2025 USENIX Annual Technical Conference (ATC)","author":"Peng Yuke","year":"2025","unstructured":"Yuke Peng, Hongliang Tian, Junyang Zhang, Ruihan Li, Chengjun Chen, Jianfeng Jiang, Jinyi Xian, Xiaolin Wang, Chenren Xu, Diyu Zhou, Yingwei Luo, Shoumeng Yan, and Yinqian Zhang. ASTERINAS: A Linux ABI-Compatible, Rust-Based Framekernel OS with a Small and Sound TCB. In Proceedings of the 2025 USENIX Annual Technical Conference (ATC), Boston, MA, July 2025."},{"key":"e_1_3_2_1_80_1","volume-title":"Peterson and Abraham Silberschatz. Operating System Concepts","author":"James","year":"1985","unstructured":"James L. Peterson and Abraham Silberschatz. Operating System Concepts. Addison-Wesley Longman Publishing Co., Inc., USA, 2 edition, 1985."},{"key":"e_1_3_2_1_81_1","first-page":"64","volume-title":"Trusted Execution Environment: What It Is, and What It Is Not. In 2015 IEEE Trustcom\/BigDataSE\/Ispa","author":"Sabt Mohamed","unstructured":"Mohamed Sabt, Mohammed Achemlal, and Abdelmadjid Bouabdallah. Trusted Execution Environment: What It Is, and What It Is Not. In 2015 IEEE Trustcom\/BigDataSE\/Ispa, volume 1, pages 57\u201364. IEEE, 2015."},{"key":"e_1_3_2_1_82_1","volume-title":"Cooperative CiteSeer. In Proceedings of the 3rd USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Stribling Jeremy","year":"2006","unstructured":"Jeremy Stribling, Jinyang Li, Isaac G Councill, M Frans Kaashoek, and Robert Tappan Morris. OverCite: A Distributed, Cooperative CiteSeer. In Proceedings of the 3rd USENIX Symposium on Networked Systems Design and Implementation (NSDI), San Jose, CA, May 2006."},{"key":"e_1_3_2_1_83_1","first-page":"200","volume-title":"Proceedings of the 15th ACM Symposium on Operating Systems Principles (SOSP)","author":"Talluri Madhusudhan","year":"1995","unstructured":"Madhusudhan Talluri, Mark D. Hill, and Yousef A. Khalidi. A New Page Table for 64-Bit Address Spaces. In Proceedings of the 15th ACM Symposium on Operating Systems Principles (SOSP), pages 184\u2013200, Copper Mountain, CO, December 1995."},{"key":"e_1_3_2_1_84_1","volume-title":"Modern Operating Systems. Pearson Education","author":"Tanenbaum Andrew S","year":"2015","unstructured":"Andrew S Tanenbaum and Herbert Bos. Modern Operating Systems. Pearson Education, Inc., 2015."},{"key":"e_1_3_2_1_85_1","first-page":"881","volume-title":"Proceedings of the 28th ACM Symposium on Operating Systems Principles (SOSP)","author":"Tao Runzhou","year":"2021","unstructured":"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 28th ACM Symposium on Operating Systems Principles (SOSP), pages 866\u2013881, Koblenz, Germany, October 2021."},{"key":"e_1_3_2_1_86_1","first-page":"91","volume-title":"A Practical Course on Operating Systems","author":"Theaker Colin J","unstructured":"Colin J Theaker and Graham R Brookes. Memory Management\u2014Segmentation. In A Practical Course on Operating Systems, pages 77\u201391. Springer, 1983."},{"key":"e_1_3_2_1_87_1","volume-title":"\/proc\/<n>\/maps getting_VERY_long","author":"Torvalds Linus","year":"2001","unstructured":"Linus Torvalds. Re: \/proc\/<n>\/maps getting_VERY_long, 2001. https:\/\/yarchive.net\/comp\/linux\/VMAs.html."},{"key":"e_1_3_2_1_88_1","first-page":"222","volume-title":"Proceedings of the 17th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Volos Haris","year":"2012","unstructured":"Haris Volos, Andres Tack, Jaan, Michael M. Swift, and Shan Lu. Applying transactional memory to concurrency bugs. In Proceedings of the 17th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 211\u2013222, London, UK, March 2012."},{"issue":"10","key":"e_1_3_2_1_89_1","article-title":"A Comprehensive Study on Security Bug Characteristics","volume":"33","author":"Wei Ying","year":"2021","unstructured":"Ying Wei, Xiaobing Sun, Lili Bo, Sicong Cao, Xin Xia, and Bin Li. A Comprehensive Study on Security Bug Characteristics. Journal of Software: Evolution and Process, 33(10), 2021.","journal-title":"Journal of Software: Evolution and Process"},{"key":"e_1_3_2_1_90_1","first-page":"110","volume-title":"Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"Yang Jean","year":"2010","unstructured":"Jean Yang and Chris Hawblitzel. Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 99\u2013110, Toronto, ON, Canada, June 2010."}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","location":"Lotte Hotel World Seoul Republic of Korea","acronym":"SOSP '25","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"]},"container-title":["Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles"],"original-title":[],"deposited":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:44:12Z","timestamp":1759322652000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3731569.3764836"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,12]]},"references-count":90,"alternative-id":["10.1145\/3731569.3764836","10.1145\/3731569"],"URL":"https:\/\/doi.org\/10.1145\/3731569.3764836","relation":{},"subject":[],"published":{"date-parts":[[2025,10,12]]},"assertion":[{"value":"2025-10-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}