A User-Mode Scheduling Mechanism for ARINC653 Partitioning in seL4
seL4 is formally verified for its functional correctness and provides a trusted code base for ARINC 653 partitioning operating systems. ARINC 653 needs a two-level scheduler to enforce temporal isolation between partitions. We cannot modify the scheduler provided by seL4 to adapt ARINC 653, which may invalidate the formal correctness of seL4. Thus, we propose a user-mode scheduling mechanism, where several user threads serve as the partition scheduler and process schedulers. The execution trace result shows that the temporal partitioning can be enforced by this mechanism. We also elaborate the scheduling overheads.
KeywordsARINC 653 sel4 Partitioning Hierarchical scheduling
This work was supported by National Natural Science Foundation of China (No. 61272167).
- 1.Radio, A. (2008). Avionics Application Software Standard Interface Part 1 - Required Services.Google Scholar
- 2.Morgan, M. J. (1991). Integrated Modular Avionics for Next-Generation Commercial Airplanes. IEEE Aerospace and Electronic Systems Magazine, 6(8), 9–12.Google Scholar
- 3.Kaiser, R., and Wagner, S. (2007). Evolution of the PikeOS microkernel. In International Workshop on Microkernels for Embedded Systems (p. 50). National ICT Australia.Google Scholar
- 4.Han, S., and Jin, H. (2012). Kernel-level ARINC 653 partitioning for Linux. In Proceedings of the 27th Annual ACM Symposium on Applied Computing – SAC12, 1632–1637.Google Scholar
- 5.VanderLeest, S. H. (2010). ARINC 653 hypervisor. AIAA/IEEE Digital Avionics Systems Conference, 1–20.Google Scholar
- 6.Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Winwood, S. (2009). seL4: Formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating System Principles, 207–220. ACM.Google Scholar
- 7.Sewell, T. A. L., Myreen, M. O., & Klein, G. (2013). Translation Validation for a Verified OS Kernel. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 471–482).Google Scholar
- 8.Boyton, A., Andronick, J., Bannister, C., Fernandez, M., Gao, X., Greenaway, D., … Sewell, T. (2013). Formally verified system initialisation. Lecture Notes in Computer Science, 8144 LNCS, 70–85.Google Scholar
- 9.Sewell, T., Winwood, S., Gammie, P., & Murray, T. (2011). seL4 Enforces Integrity. In 2nd ITP (pp. 325–340). LNCS.Google Scholar
- 10.Murray, T., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., … Klein, G. (2013). seL4: From general purpose to a proof of information flow enforcement. Proceedings - IEEE Symposium on Security and Privacy, 415–429.Google Scholar
- 11.Åsberg, M., and Nolte, T. (2013). Towards a User-Mode Approach to Partitioned Scheduling in the seL4 Microkernel. 5th International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems, 15–22.Google Scholar
- 12.Lyons, A., and Heiser, G. (2014). Mixed-Criticality Support in a High-Assurance, General-Purpose Microkernel. Workshop on Mixed Criticality Systems, 9–14.Google Scholar