{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T03:19:47Z","timestamp":1752981587353,"version":"3.41.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1945541; 2019285; 2118851"],"award-info":[{"award-number":["1945541; 2019285; 2118851"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"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"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>Real-time systems power safety-critical applications that require strong isolation among each other. Such isolation needs to be enforced at two orthogonal levels. On the micro-architectural level, this mainly involves avoiding interference through micro-architectural states, such as cache lines. On the algorithmic level, this is usually achieved by adopting real-time partitions to reserve resources for each application. Implementations of such systems are often complex and require formal verification to guarantee proper isolation.<\/jats:p>\n          <jats:p>In this paper, we focus on algorithmic isolation, which is mainly related to scheduling-induced interferences. We address earliest-deadline-first (EDF) partitions to achieve compositionality and utilization, while imposing constraints on tasks' periods and enforcing budgets on these periodic partitions to ensure isolation between each other. The formal verification of such a real-time OS kernel is challenging due to the inherent complexity of the dynamic priority assignment on the partition level. We tackle this problem by adopting a dynamically constructed abstraction to lift the reasoning of a concrete scheduler into an abstract domain. Using this framework, we verify a real-time operating system kernel with budget-enforcing EDF partitions and prove that it indeed ensures isolation between partitions. All the proofs are mechanized in Coq.<\/jats:p>","DOI":"10.1145\/3563290","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"60-88","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7027-4566","authenticated-orcid":false,"given":"Mengqi","family":"Liu","sequence":"first","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8184-7649","authenticated-orcid":false,"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1180-9433","authenticated-orcid":false,"given":"Hao","family":"Chen","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7181-1730","authenticated-orcid":false,"given":"Man-Ki","family":"Yoon","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9780-2947","authenticated-orcid":false,"given":"Jung-Eun","family":"Kim","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1998.739726"},{"key":"e_1_2_1_2_1","unstructured":"2010. Avionics Application Software Standard Interface: ARINC Specification 653P1-3. \t\t\t\t  2010. Avionics Application Software Standard Interface: ARINC Specification 653P1-3."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_4"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2016.28"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2005.25"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/EMWRTS.1997.613785"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.2000.896005"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2018.00039"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303976"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3356903"},{"key":"e_1_2_1_13_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) . USENIX Association, Savannah, GA. 653\u2013669. isbn:978-1-93 1971-33-1 https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu 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). USENIX Association, Savannah, GA. 653\u2013669. isbn:978-1-931971-33-1 https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_28"},{"key":"e_1_2_1_15_1","unstructured":"Gernot Heiser. 2020. The seL4 Microkernel \u2013 An Introduction (White paper). Revision 1.2. June. \t\t\t\t  Gernot Heiser. 2020. The seL4 Microkernel \u2013 An Introduction (White paper). Revision 1.2. June."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3317550.3321431"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/29.5.390"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2015.7108445"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1989.63567"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/321738.321743"},{"key":"e_1_2_1_22_1","volume-title":"Real-Time Systems","author":"Liu Jane W. S. W.","unstructured":"Jane W. S. W. Liu . 2000. Real-Time Systems ( 1 st ed.). Prentice Hall PTR , Upper Saddle River, NJ, USA. isbn:0130996513 Jane W. S. W. Liu. 2000. Real-Time Systems (1st ed.). Prentice Hall PTR, Upper Saddle River, NJ, USA. isbn:0130996513","edition":"1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371088"},{"key":"e_1_2_1_24_1","unstructured":"2022. LynxOS-178.  https:\/\/www.lynx.com\/products\/lynxos-178-do-178c-certified-posix-rtos \t\t\t\t  2022. LynxOS-178.  https:\/\/www.lynx.com\/products\/lynxos-178-do-178c-certified-posix-rtos"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3190508.3190539"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECRTS.2022.19"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECRTS.2022.5"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2016.271"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.2003.1253249"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02341920"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS54340.2022.00030"},{"key":"e_1_2_1_34_1","unstructured":"2022. Wind River VxWorks 653 Platform.  https:\/\/www.windriver.com\/products\/vxworks\/certification-profiles\/#vxworks_653 \t\t\t\t  2022. Wind River VxWorks 653 Platform.  https:\/\/www.windriver.com\/products\/vxworks\/certification-profiles\/#vxworks_653"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028759"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_4"},{"key":"e_1_2_1_37_1","volume-title":"Proc. 30th USENIX Security Symposium on (USENIX Security 2021)","author":"Yoon Man-Ki","year":"2021","unstructured":"Man-Ki Yoon , Mengqi Liu , Hao Chen , Jung-Eun Kim , and Zhong Shao . 2021 . Blinder: Partition-Oblivious Hierarchical Scheduling . In Proc. 30th USENIX Security Symposium on (USENIX Security 2021) , August 2021.. Man-Ki Yoon, Mengqi Liu, Hao Chen, Jung-Eun Kim, and Zhong Shao. 2021. Blinder: Partition-Oblivious Hierarchical Scheduling. In Proc. 30th USENIX Security Symposium on (USENIX Security 2021), August 2021.."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_15"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563290","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563290","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563290","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563290"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":38,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563290"],"URL":"https:\/\/doi.org\/10.1145\/3563290","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}