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.