{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:57:01Z","timestamp":1774025821418,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":56,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,10,26]],"date-time":"2021-10-26T00:00:00Z","timestamp":1635206400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["N66001-21-C-4018"],"award-info":[{"award-number":["N66001-21-C-4018"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CCF-1918400, CNS-2052947, CCF-2124080"],"award-info":[{"award-number":["CCF-1918400, CNS-2052947, CCF-2124080"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,10,26]]},"DOI":"10.1145\/3477132.3483560","type":"proceedings-article","created":{"date-parts":[[2021,10,19]],"date-time":"2021-10-19T15:59:18Z","timestamp":1634659158000},"page":"866-881","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware"],"prefix":"10.1145","author":[{"given":"Runzhou","family":"Tao","sequence":"first","affiliation":[{"name":"Columbia University, New York, NY, USA"}]},{"given":"Jianan","family":"Yao","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY, USA"}]},{"given":"Xupeng","family":"Li","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY, USA"}]},{"given":"Shih-Wei","family":"Li","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY, USA and National Taiwan University"}]},{"given":"Jason","family":"Nieh","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY, USA"}]},{"given":"Ronghui","family":"Gu","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,10,26]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the 17th Annual International Symposium on Computer Architecture (ISCA '90)","author":"Sarita","unstructured":"Sarita V. Adve and Mark D. Hill. 1990. Weak Ordering-A New Definition . In Proceedings of the 17th Annual International Symposium on Computer Architecture (ISCA '90) . 2--14. Sarita V. Adve and Mark D. Hill. 1990. Weak Ordering-A New Definition. In Proceedings of the 17th Annual International Symposium on Computer Architecture (ISCA '90). 2--14."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177156"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_5_1","volume-title":"Document Version 20191213","author":"Asanovic Krste","unstructured":"Krste Asanovic and Andrew Waterman . 2019. The RISC-V Instruction Set Manual, Volume I: User-Level ISA , Document Version 20191213 . RISC-V Foundation . Krste Asanovic and Andrew Waterman. 2019. The RISC-V Instruction Set Manual, Volume I: User-Level ISA, Document Version 20191213. RISC-V Foundation."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_1_7_1","volume-title":"Hardware and Software Support for Virtualization","author":"Bugnion Edouard","unstructured":"Edouard Bugnion , Jason Nieh , and Dan Tsafrir . 2017. Hardware and Software Support for Virtualization . Morgan and Claypool Publishers . Edouard Bugnion, Jason Nieh, and Dan Tsafrir. 2017. Hardware and Software Support for Virtualization. Morgan and Claypool Publishers."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1807128.1807152"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2016.35"},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of the 2017 USENIX Annual Technical Conference (USENIX ATC '17). 221--234","author":"Dall Christoffer","year":"2017","unstructured":"Christoffer Dall , Shih-Wei Li , and Jason Nieh . 2017 . Optimizing the Design and Implementation of the Linux ARM Hypervisor . In Proceedings of the 2017 USENIX Annual Technical Conference (USENIX ATC '17). 221--234 . Christoffer Dall, Shih-Wei Li, and Jason Nieh. 2017. Optimizing the Design and Implementation of the Linux ARM Hypervisor. In Proceedings of the 2017 USENIX Annual Technical Conference (USENIX ATC '17). 221--234."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541946"},{"key":"e_1_3_2_1_16_1","unstructured":"Will Deacon and Jade Alglave. 2020. The ARMv8 Application Level Memory Model. http:\/\/diy.inna.fr\/www\/?record=aarch64.  Will Deacon and Jade Alglave. 2020. The ARMv8 Application Level Memory Model. http:\/\/diy.inna.fr\/www\/?record=aarch64."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192421"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_2_1_19_1","first-page":"1","article-title":"Modelling the ARMv8 Architecture, Operationally","volume":"51","author":"Flur Shaked","year":"2016","unstructured":"Shaked Flur , Kathryn E. Gray , Christopher Pulte , Susmit Sarkar , Ali Sezgin , Luc Maranget , Will Deacon , and Peter Sewell . 2016 . Modelling the ARMv8 Architecture, Operationally : Concurrency and ISA. ACM SIGPLAN Notices 51 , 1 (Jan. 2016), 608--621. Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. 2016. Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA. ACM SIGPLAN Notices 51, 1 (Jan. 2016), 608--621.","journal-title":"Concurrency and ISA. ACM SIGPLAN Notices"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_1_22_1","first-page":"10","article-title":"Building Certified Concurrent OS","volume":"62","author":"Gu Ronghui","year":"2019","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Jieung Kim , J\u00e9r\u00e9mie Koenig , Xiongnan Wu , Vilhelm Sj\u00f6berg , and David Costanzo . 2019 . Building Certified Concurrent OS Kernels. Commun. ACM 62 , 10 (Sept. 2019), 89--99. Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, J\u00e9r\u00e9mie Koenig, Xiongnan Wu, Vilhelm Sj\u00f6berg, and David Costanzo. 2019. Building Certified Concurrent OS Kernels. Commun. ACM 62, 10 (Sept. 2019), 89--99.","journal-title":"Kernels. Commun. ACM"},{"key":"e_1_3_2_1_23_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI '16)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan Newman Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI '16) . 653--669. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI '16). 653--669."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"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","unstructured":"Andrew Jones Paolo Bonzini and Thomas Huth. 2020. KVM Unit Tests. http:\/\/www.linux-kvm.org\/page\/KVM-unit-tests.  Andrew Jones Paolo Bonzini and Thomas Huth. 2020. KVM Unit Tests. http:\/\/www.linux-kvm.org\/page\/KVM-unit-tests."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_14"},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the 2007 Ottawa Linux Symposium (OLS '07)","author":"Kivity Avi","year":"2007","unstructured":"Avi Kivity , Yaniv Kamay , Dor Laor , Uri Lublin , and Anthony Liguori . 2007 . KVM: the Linux Virtual Machine Monitor . In Proceedings of the 2007 Ottawa Linux Symposium (OLS '07) . 225--230. Avi Kivity, Yaniv Kamay, Dor Laor, Uri Lublin, and Anthony Liguori. 2007. KVM: the Linux Virtual Machine Monitor. In Proceedings of the 2007 Ottawa Linux Symposium (OLS '07). 225--230."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385966"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"e_1_3_2_1_35_1","volume-title":"Proceedings of the 28th USENIX Security Symposium (USENIX Security '19)","author":"Li Shih-Wei","year":"2019","unstructured":"Shih-Wei Li , John S. Koh , and Jason Nieh . 2019 . Protecting Cloud Virtual Machines from Commodity Hypervisor and Host Operating System Exploits . In Proceedings of the 28th USENIX Security Symposium (USENIX Security '19) . 1357--1374. Shih-Wei Li, John S. Koh, and Jason Nieh. 2019. Protecting Cloud Virtual Machines from Commodity Hypervisor and Host Operating System Exploits. In Proceedings of the 28th USENIX Security Symposium (USENIX Security '19). 1357--1374."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00049"},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the 30th USENIX Security Symposium (USENIX Security '21)","author":"Li Shih-Wei","year":"2021","unstructured":"Shih-Wei Li , Xupeng Li , Ronghui Gu , Jason Nieh , and John Zhuang Hui . 2021 . Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor . In Proceedings of the 30th USENIX Security Symposium (USENIX Security '21) . 3953--3970. Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. 2021. Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. In Proceedings of the 30th USENIX Security Symposium (USENIX Security '21). 3953--3970."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132754"},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the ACM on Programming Languages 4, POPL (Jan.","author":"Liu Mengqi","year":"2019","unstructured":"Mengqi Liu , Lionel Rieg , Zhong Shao , Ronghui Gu , David Costanzo , Jung-Eun Kim , and Man-Ki Yoon . 2019 . Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation . Proceedings of the ACM on Programming Languages 4, POPL (Jan. 2019), 1--31. Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon. 2019. Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation. Proceedings of the ACM on Programming Languages 4, POPL (Jan. 2019), 1--31."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385971"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434285"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446748"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_1_46_1","unstructured":"Igor Pavlov. 2015. Applied Micro X-Gene. https:\/\/www.7-cpu.com\/cpu\/X-Gene.html.  Igor Pavlov. 2015. Applied Micro X-Gene. https:\/\/www.7-cpu.com\/cpu\/X-Gene.html."},{"key":"e_1_3_2_1_47_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL (Dec.","author":"Pulte Christopher","year":"2017","unstructured":"Christopher Pulte , Shaked Flur , Will Deacon , Jon French , Susmit Sarkar , and Peter Sewell . 2017 . Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 . Proceedings of the ACM on Programming Languages 2, POPL (Dec. 2017). Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. 2017. Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8. Proceedings of the ACM on Programming Languages 2, POPL (Dec. 2017)."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314624"},{"key":"e_1_3_2_1_49_1","unstructured":"Rusty Russell. 2008. Hackbench. http:\/\/people.redhat.com\/mingo\/cfs-scheduler\/tools\/hackbench.c.  Rusty Russell. 2008. Hackbench. http:\/\/people.redhat.com\/mingo\/cfs-scheduler\/tools\/hackbench.c."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_2_1_53_1","volume-title":"Nickel: A Framework for Design and Verification of Information Flow Control Systems. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI '18)","author":"Sigurbjarnarson Helgi","year":"2018","unstructured":"Helgi Sigurbjarnarson , Luke Nelson , Bruno Castro-Karney , James Bornholt , Emina Torlak , and Xi Wang . 2018 . Nickel: A Framework for Design and Verification of Information Flow Control Systems. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI '18) . 287--305. Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. 2018. Nickel: A Framework for Design and Verification of Information Flow Control Systems. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI '18). 287--305."},{"key":"e_1_3_2_1_54_1","unstructured":"The Apache Software Foundation. 2020. ab - Apache HTTP Server Benchmarking Tool. http:\/\/httpd.apache.org\/docs\/2.4\/programs\/ab.html.  The Apache Software Foundation. 2020. ab - Apache HTTP Server Benchmarking Tool. http:\/\/httpd.apache.org\/docs\/2.4\/programs\/ab.html."},{"key":"e_1_3_2_1_55_1","unstructured":"The Coq Team. 2021. The Coq Proof Assistant. http:\/\/coq.inria.fr.  The Coq Team. 2021. The Coq Proof Assistant. http:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359644"}],"event":{"name":"SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles","location":"Virtual Event Germany","acronym":"SOSP '21","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX Assoc USENIX Assoc"]},"container-title":["Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477132.3483560","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3477132.3483560","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3477132.3483560","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:49:15Z","timestamp":1750193355000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477132.3483560"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,26]]},"references-count":56,"alternative-id":["10.1145\/3477132.3483560","10.1145\/3477132"],"URL":"https:\/\/doi.org\/10.1145\/3477132.3483560","relation":{},"subject":[],"published":{"date-parts":[[2021,10,26]]},"assertion":[{"value":"2021-10-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}