Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation
Article No.: 127, Pages 60 - 88
Abstract
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.
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.
References
[1]
L. Abeni and G. Buttazzo. 1998. Integrating multimedia applications in hard real-time systems. In Proceedings 19th IEEE Real-Time Systems Symposium. 4–13. https://doi.org/10.1109/REAL.1998.739726
[2]
2010. Avionics Application Software Standard Interface: ARINC Specification 653P1-3.
[3]
June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, and Christine Rizkallah. 2016. Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. In Proceedings of 7th International Conference on Interactive Theorem Proving (ITP). Springer International Publishing, Nancy, France. 52–68. isbn:978-3-319-43144-4 https://doi.org/10.1007/978-3-319-43144-4_4
[4]
F. Cerqueira, F. Stutz, and B. B. Brandenburg. 2016. PROSA: A Case for Readable Mechanized Schedulability Analysis. In 2016 28th Euromicro Conference on Real-Time Systems (ECRTS). 273–284. https://doi.org/10.1109/ECRTS.2016.28
[5]
David Costanzo, Zhong Shao, and Ronghui Gu. 2016. End-to-end Verification of Information-flow Security for C and Assembly Programs. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). ACM, New York, NY, USA. 648–664. isbn:978-1-4503-4261-2 https://doi.org/10.1145/2908080.2908100
[6]
R. I. Davis and A. Burns. 2005. Hierarchical Fixed Priority Pre-Emptive Scheduling. In Proceedings of the 26th IEEE International Real-Time Systems Symposium (RTSS’05). IEEE Computer Society, Washington, DC, USA. 389–398. isbn:0-7695-2490-7 https://doi.org/10.1109/RTSS.2005.25
[7]
Z. Deng, J.W.-S. Liu, and J. Sun. 1997. A scheme for scheduling hard real-time applications in open system environment. In Proceedings Ninth Euromicro Workshop on Real Time Systems. 191–199. https://doi.org/10.1109/EMWRTS.1997.613785
[8]
B. Dutertre. 2000. Formal analysis of the priority ceiling protocol. In Proceedings 21st IEEE Real-Time Systems Symposium (RTSS’00). IEEE Computer Society, Washington, DC. 151–160. issn:1052-8725 https://doi.org/10.1109/REAL.2000.896005
[9]
Pascal Fradet, Maxime Lesourd, Jean-François Monin, and Sophie Quinton. 2018. A Generic Coq Proof of Typical Worst-Case Analysis. In 2018 IEEE Real-Time Systems Symposium (RTSS). 218–229. https://doi.org/10.1109/RTSS.2018.00039
[10]
Qian Ge, Yuval Yarom, Tom Chothia, and Gernot Heiser. 2019. Time Protection: The Missing OS Abstraction. In Proceedings of the Fourteenth EuroSys Conference 2019 (EuroSys’19). ACM, New York, NY, USA. Article 1, 17 pages. isbn:978-1-4503-6281-8 https://doi.org/10.1145/3302424.3303976
[11]
Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). ACM, New York, NY, USA. 595–608. isbn:978-1-4503-3300-9 https://doi.org/10.1145/2676726.2676975
[12]
Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jérémie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjöberg, and David Costanzo. 2019. Building Certified Concurrent OS Kernels. Commun. ACM, 62, 10 (2019), sep, 89–99. issn:0001-0782 https://doi.org/10.1145/3356903
[13]
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, 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–669. isbn:978-1-931971-33-1 https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu
[14]
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’19), July 15-18, Proceedings. Springer, Berlin, Heidelberg. 496–514. https://doi.org/10.1007/978-3-030-25543-5_28
[15]
Gernot Heiser. 2020. The seL4 Microkernel – An Introduction (White paper). Revision 1.2. June.
[16]
Gernot Heiser, Gerwin Klein, and Toby Murray. 2019. Can We Prove Time Protection? In Proceedings of the Workshop on Hot Topics in Operating Systems (HotOS ’19). Association for Computing Machinery, New York, NY, USA. 23–29. isbn:9781450367271 https://doi.org/10.1145/3317550.3321431
[17]
Mathai Joseph and Paritosh Pandya. 1986. Finding response times in a real-time system. Comput. J., 29, 5 (1986), 390–395. https://doi.org/10.1093/comjnl/29.5.390
[18]
Jung-Eun Kim, Tarek Abdelzaher, and Lui Sha. 2015. Budgeted generalized rate monotonic analysis for the partitioned, yet globally scheduled uniprocessor model. In 21st IEEE Real-Time and Embedded Technology and Applications Symposium. 221–231. https://doi.org/10.1109/RTAS.2015.7108445
[19]
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. 2009. SeL4: Formal Verification of an OS Kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP ’09). Association for Computing Machinery, New York, NY, USA. 207–220. isbn:9781605587523 https://doi.org/10.1145/1629575.1629596
[20]
J. Lehoczky, L. Sha, and Y. Ding. 1989. The rate monotonic scheduling algorithm: exact characterization and average case behavior. In [1989] Proceedings. Real-Time Systems Symposium. 166–171. https://doi.org/10.1109/REAL.1989.63567
[21]
C. L. Liu and James W. Layland. 1973. Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment. J. ACM, 20, 1 (1973), Jan., 46–61. issn:0004-5411 https://doi.org/10.1145/321738.321743
[22]
Jane W. S. W. Liu. 2000. Real-Time Systems (1st ed.). Prentice Hall PTR, Upper Saddle River, NJ, USA. isbn:0130996513
[23]
Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon. 2020. Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation. Proc. ACM Program. Lang., 4, POPL (2020), Jan., 31 pages. https://doi.org/10.1145/3371088
[24]
2022. LynxOS-178. https://www.lynx.com/products/lynxos-178-do-178c-certified-posix-rtos
[25]
Anna Lyons, Kent McLeod, Hesham Almatary, and Gernot Heiser. 2018. Scheduling-Context Capabilities: A Principled, Light-Weight Operating-System Mechanism for Managing Time. In Proceedings of the Thirteenth EuroSys Conference (EuroSys ’18). Association for Computing Machinery, New York, NY, USA. Article 26, 16 pages. isbn:9781450355841 https://doi.org/10.1145/3190508.3190539
[26]
Marco Maida, Sergey Bozhko, and Björn B. Brandenburg. 2022. Foundational Response-Time Analysis as Explainable Evidence of Timeliness. In 34th Euromicro Conference on Real-Time Systems (ECRTS 2022), Martina Maggio (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 231). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 19:1–19:25. isbn:978-3-95977-239-6 issn:1868-8969 https://doi.org/10.4230/LIPIcs.ECRTS.2022.19
[27]
Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. 2013. seL4: From General Purpose to a Proof of Information Flow Enforcement. In 2013 IEEE Symposium on Security and Privacy (SP’13), Berkeley, CA, USA, May 19-22, 2013. IEEE Computer Society, Washington, DC. 415–429. https://doi.org/10.1109/SP.2013.35
[28]
Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. 2017. Hyperkernel: Push-Button Verification of an OS Kernel. In Proceedings of the 26th Symposium on Operating Systems Principles (SOSP’17), Shanghai, China, October 28-31, 2017. ACM, New York, NY, USA. 252–269. isbn:978-1-4503-5085-3 https://doi.org/10.1145/3132747.3132748
[29]
Pierre Roux, Sophie Quinton, and Marc Boyer. 2022. A Formal Link Between Response Time Analysis and Network Calculus. In 34th Euromicro Conference on Real-Time Systems (ECRTS 2022), Martina Maggio (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 231). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 5:1–5:22. isbn:978-3-95977-239-6 issn:1868-8969 https://doi.org/10.4230/LIPIcs.ECRTS.2022.5
[30]
L. Sha, M. Caccamo, R. Mancuso, J. E. Kim, M. K. Yoon, R. Pellizzoni, H. Yun, R. B. Kegley, D. R. Perlman, G. Arundale, and R. Bradford. 2016. Real-Time Computing on Multicore Processors. Computer, 49, 9 (2016), Sept, 69–77. issn:0018-9162 https://doi.org/10.1109/MC.2016.271
[31]
Insik Shin and Insup Lee. 2003. Periodic resource model for compositional real-time guarantees. In RTSS 2003. 24th IEEE Real-Time Systems Symposium, 2003. 2–13. https://doi.org/10.1109/REAL.2003.1253249
[32]
Brinkley Sprunt, Lui Sha, and John Lehoczky. 1989. Aperiodic task scheduling for Hard-Real-Time systems. Journal of Real-Time Systems, 1 (1989), 27–60. https://doi.org/10.1007/BF02341920
[33]
Florian Vanhems, Vlad Rusu, David Nowak, and Gilles Grimaud. 2022. A Formal Correctness Proof for an EDF Scheduler Implementation. In 2022 IEEE 28th Real-Time and Embedded Technology and Applications Symposium (RTAS). 281–292. https://doi.org/10.1109/RTAS54340.2022.00030
[34]
2022. Wind River VxWorks 653 Platform. https://www.windriver.com/products/vxworks/certification-profiles/#vxworks_653
[35]
Matthew Wilding. 1998. A machine-checked proof of the optimality of a real-time scheduling policy. In Computer Aided Verification, Alan J. Hu and Moshe Y. Vardi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 369–378. isbn:978-3-540-69339-0 https://doi.org/10.1007/BFb0028759
[36]
Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li. 2016. A Practical Verification Framework for Preemptive OS Kernels. In Computer Aided Verification: 28th International Conference (CAV’16), Toronto, ON, Canada, July 17-23, 2016, Proceedings, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Berlin, Heidelberg. 59–79. isbn:978-3-319-41540-6 https://doi.org/10.1007/978-3-319-41540-6_4
[37]
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.
[38]
Xingyuan Zhang, Christian Urban, and Chunhan Wu. 2012. Priority Inheritance Protocol Proved Correct. In Interactive Theorem Proving (ITP’12). Springer, Berlin, Heidelberg. 217–232. isbn:978-3-642-32347-8 https://doi.org/10.1007/978-3-642-32347-8_15
Index Terms
- Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation
Recommendations
Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation
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 ...
Global and Partitioned Multiprocessor Fixed Priority Scheduling with Deferred Preemption
Special Issue on Embedded Platforms for Crypto and Regular PapersThis article introduces schedulability analysis for Global Fixed Priority Scheduling with Deferred Preemption (gFPDS) for homogeneous multiprocessor systems. gFPDS is a superset of Global Fixed Priority Preemptive Scheduling (gFPPS) and Global Fixed ...
An $\mathsf{EDF}$ -based restricted-migration scheduling algorithm for multiprocessor soft real-time systems
There has been much recent interest in the use of the earliest-deadline-first ( $\mathsf{EDF}$ ) algorithm for scheduling soft real-time sporadic task systems on identical multiprocessors. In hard real-time systems, a significant disparity exists between $\mathsf{EDF}$ -based ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2022
1932 pages
Copyright © 2022 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 31 October 2022
Published in PACMPL Volume 6, Issue OOPSLA2
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 230Total Downloads
- Downloads (Last 12 months)118
- Downloads (Last 6 weeks)21
Reflects downloads up to 14 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in