Towards Fault-Tolerant Real-Time Scheduling in the seL4 Microkernel
Libin Xu, Yuebin Bai, Kun Cheng, Lingyu Ge, Danning Nie, Lijun Zhang, Wenjia Liu · 2016
System dependability and real-time requirement have been receiving widespread attention in modern computer systems. Fault-tolerant real-time scheduling provides a method of combining timing requirements and faults tolerance for real-time systems. This paper presents a preliminary study of building a fault-tolerant real-time mechanism for seL4 microkernel. seL4, as the first formally-verified operating system kernel in the world, is an ideal platform for security-critical systems. However, the lack of real-time and fault-tolerant policy reduces its the reliability and user experience. We have implemented basic real-time and checkpoint mechanisms in seL4, and propose the Check-Point based Fault-Tolerant RM (CP-FTRM) scheduling policy. The experiments have shown the feasibility and efficiency of them.