{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T16:20:52Z","timestamp":1781713252034,"version":"3.54.5"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-16-2-0274, FA8750-15-C-0082"],"award-info":[{"award-number":["FA8750-16-2-0274, FA8750-15-C-0082"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"name":"PEPS INS2I JCJC","award":["2019 Vefose"],"award-info":[{"award-number":["2019 Vefose"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1521523, 1715154, 1763399"],"award-info":[{"award-number":["1521523, 1715154, 1763399"]}],"id":[{"id":"10.13039\/100000001","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":[[2020,1]]},"abstract":"<jats:p>\n            The reliability and security of safety-critical real-time systems are of utmost importance because the failure of these systems could incur severe consequences (e.g., loss of lives or failure of a mission). Such properties require strong isolation between components and they rely on enforcement mechanisms provided by the underlying operating system (OS) kernel. In addition to spatial isolation which is commonly provided by OS kernels to various extents, it also requires temporal isolation, that is, properties on the schedule of one component (e.g., schedulability) are independent of behaviors of other components. The strict isolation between components relies critically on algorithmic properties of the\n            <jats:italic>concrete implementation<\/jats:italic>\n            of the scheduler, such as timely provision of time slots, obliviousness to preemption, etc. However, existing work either only reasons about an abstract model of the scheduler, or proves properties of the scheduler implementation that are not rich enough to establish the isolation between different components.\n          <\/jats:p>\n          <jats:p>\n            In this paper, we present a novel compositional framework for reasoning about algorithmic properties of the concrete implementation of preemptive schedulers. In particular, we use\n            <jats:italic>virtual timeline<\/jats:italic>\n            , a variant of the supply bound function used in real-time scheduling analysis, to specify and reason about the scheduling of each component in isolation. We show that the properties proved on this abstraction carry down to the generated assembly code of the OS kernel. Using this framework, we successfully verify a real-time OS kernel, which extends mCertiKOS, a single-processor non-preemptive kernel, with user-level preemption, a verified timer interrupt handler, and a verified real-time scheduler. We prove that in the absence of microarchitectural-level timing channels, this new kernel enjoys temporal and spatial isolation on top of the functional correctness guarantee. All the proofs are implemented in the Coq proof assistant.\n          <\/jats:p>","DOI":"10.1145\/3371088","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation"],"prefix":"10.1145","volume":"4","author":[{"given":"Mengqi","family":"Liu","sequence":"first","affiliation":[{"name":"Yale University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lionel","family":"Rieg","sequence":"additional","affiliation":[{"name":"Grenoble Alps University, France \/ CNRS, France \/ Grenoble INP, France \/ VERIMAG, France \/ Yale University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ronghui","family":"Gu","sequence":"additional","affiliation":[{"name":"Columbia University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Costanzo","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jung-Eun","family":"Kim","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Man-Ki","family":"Yoon","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_4"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.196.2"},{"key":"e_1_2_2_3_1","volume-title":"ARINC Specification 653 Part 1","author":"ARINC.","unstructured":"ARINC. 2015. ARINC Specification 653 Part 1 . ARINC , Annapolis, MD . ARINC. 2015. ARINC Specification 653 Part 1. ARINC, Annapolis, MD."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.38"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_31"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2016.28"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2005.25"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.2000.896005"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303976"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_2_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\u201916)","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\u201916) . USENIX Association, GA, 653\u2013669. 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\u201916). USENIX Association, GA, 653\u2013669."},{"key":"e_1_2_2_14_1","volume-title":"Certified Concurrent Abstraction Layers. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI","author":"Gu Ronghui","year":"2018","unstructured":"Ronghui Gu , Zhong Shao , Jieung Kim , Xiongnan Wu , J\u00e9r\u00e9mie Koenig , Vilhelm Sj\u00f6berg , Hao Chen , David Costanzo , and Tahina Ramananandro . 2018 . Certified Concurrent Abstraction Layers. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018). ACM, New York, 646\u2013661. Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan Wu, J\u00e9r\u00e9mie Koenig, Vilhelm Sj\u00f6berg, Hao Chen, David Costanzo, and Tahina Ramananandro. 2018. Certified Concurrent Abstraction Layers. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018). ACM, New York, 646\u2013661."},{"key":"e_1_2_2_15_1","volume-title":"Proceedings. Springer","author":"Guo Xiaojie","year":"2019","unstructured":"Xiaojie Guo , Maxime Lesourd , Mengqi Liu , Lionel Rieg , and Zhong Shao . 2019 . Integrating Formal Schedulability Analysis into a Verified OS Kernel. In Computer Aided Verification - 31st International Conference (CAV\u201919), July 15-18 , Proceedings. Springer , Berlin, Heidelberg, 496\u2013514. Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, and Zhong Shao. 2019. Integrating Formal Schedulability Analysis into a Verified OS Kernel. In Computer Aided Verification - 31st International Conference (CAV\u201919), July 15-18, Proceedings. Springer, Berlin, Heidelberg, 496\u2013514."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2015.7108445"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0002-4"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_2_19_1","volume-title":"Jean J. Labrosse. 1998. Microc\/OS-II","unstructured":"Jean J. Labrosse. 1998. Microc\/OS-II ( 2 nd ed.). Focal Press , New York . Jean J. Labrosse. 1998. Microc\/OS-II (2nd ed.). Focal Press, New York.","edition":"2"},{"key":"e_1_2_2_20_1","unstructured":"Jean J. Labrosse. 2011. Microc\/OS-III. Micrium Press Austin TX.  Jean J. Labrosse. 2011. Microc\/OS-III. Micrium Press Austin TX."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1989.63567"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_23_1","volume-title":"Program Logics for Certified Compilers, Andrew W","author":"Leroy Xavier","unstructured":"Xavier Leroy , Andrew W. Appel , Sandrine Blazy , and Gordon Stewart . 2014. The CompCert memory model . In Program Logics for Certified Compilers, Andrew W . Appel (Ed.). Cambridge University Press, Cambridge , UK. http:\/\/vst.cs.princeton.edu\/ Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. 2014. The CompCert memory model. In Program Logics for Certified Compilers, Andrew W. Appel (Ed.). Cambridge University Press, Cambridge, UK. http:\/\/vst.cs.princeton.edu\/"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/321738.321743"},{"key":"e_1_2_2_25_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. Jane W. S. W. Liu. 2000. Real-Time Systems (1st ed.). Prentice Hall PTR, Upper Saddle River, NJ, USA.","edition":"1"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3190508.3190539"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46078-8_48"},{"key":"e_1_2_2_30_1","unstructured":"QNX. 2019. Neutrino RTOS. http:\/\/blackberry.qnx.com\/en\/products\/neutrino- rtos\/neutrino- rtos  QNX. 2019. Neutrino RTOS. http:\/\/blackberry.qnx.com\/en\/products\/neutrino- rtos\/neutrino- rtos"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-1539-9_10"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-017-9286-3"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2016.271"},{"key":"e_1_2_2_35_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\u201918)","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\u201918) . USENIX Association, Carlsbad, CA, 287\u2013305. 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\u201918). USENIX Association, Carlsbad, CA, 287\u2013305."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/647767.733638"},{"key":"e_1_2_2_38_1","volume-title":"Proceedings of the Ninth ACM International Conference on Embedded Software (EMSOFT). ACM","author":"Xi S.","unstructured":"S. Xi , J. Wilson , C. Lu , and C. Gill . 2011. RT-Xen: Towards real-time hypervisor scheduling in Xen . In Proceedings of the Ninth ACM International Conference on Embedded Software (EMSOFT). ACM , New York, 39\u201348. S. Xi, J. Wilson, C. Lu, and C. Gill. 2011. RT-Xen: Towards real-time hypervisor scheduling in Xen. In Proceedings of the Ninth ACM International Conference on Embedded Software (EMSOFT). ACM, New York, 39\u201348."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_4"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/1267308.1267327"},{"key":"e_1_2_2_41_1","volume-title":"Interactive Theorem Proving (ITP\u201912)","author":"Zhang Xingyuan","unstructured":"Xingyuan Zhang , Christian Urban , and Chunhan Wu. 2012. Priority Inheritance Protocol Proved Correct . In Interactive Theorem Proving (ITP\u201912) . Springer, Berlin , Heidelberg , 217\u2013232. Xingyuan Zhang, Christian Urban, and Chunhan Wu. 2012. Priority Inheritance Protocol Proved Correct. In Interactive Theorem Proving (ITP\u201912). Springer, Berlin, Heidelberg, 217\u2013232."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-016-4226-2"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371088","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371088","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371088","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371088"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":41,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371088"],"URL":"https:\/\/doi.org\/10.1145\/3371088","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}