A Practical Verification Framework for Preemptive OS Kernels 61 Fifth,we also specify and verify priority inversion freedom (PIF)of uC/OS-II.PIF is a crucial property for real-time systems and is worth veri- fying in its own right.Moreover,since the specification and verification are done at the level of the abstract model (i.e.,specifications)of the kernel,they also help validate our model of system APIs.As we explain above,many important properties cannot be specified if the model is too weak or overly abstract. Coq proofs and a companion technical report are available at http://staff. ustc.edu.cn/~fuming/research/certiucos. 2 Background and Overview of Our Work 2.1 Preemptive OS Kernels and Interrupts In a preemptive OS kernel,execution of a task inside the kernel can be inter- rupted at any program point (unless interrupts are disabled).Then the control is switched to the interrupt handler.When the handler finishes,it may invoke the scheduler and switch the execution context to a different task,instead of return- ing to the original interrupted task.For instance,with priority-based scheduling, the interrupt handler always switches to the highest priority task at its end. The x86 Interrupt Mechanism.Interrupt handling and management are indis- pensable in preemptive OS kernels.We give an overview of the interrupt mech- anism in x86 systems (based on the Intel 8259 A interrupt controller). The CPU has a flag bit IF indicating whether interrupts are enabled or not. The cli/sti instruction clears/sets the bit to disable/enable interrupts.In 8259 A there is a register isr,each bit of which corresponds to a hardware interrupt and records if the interrupt is being served or not.Different priority levels are assigned to different sources of interrupts,with level-0 being the highest.When an interrupt request comes,we check IF and isr.If the interrupts are enabled and there is currently no interrupt with higher or the same priority being served, the request will be served.The corresponding bit in isr is set to 1 and the control jumps to the corresponding interrupt handler. On the invocations of an interrupt handler,the CPU flags (including IF)are saved on the stack,and interrupts are disabled automatically.If interrupts are enabled again inside the handler,the handler could be further interrupted by requests with higher priorities,causing nested interrupts. The handler returns to the program being interrupted using the iret instruc- tion,which also restores the flags (including IF).Before the handler returns, it needs to execute eoi to send an "end of interrupt"signal to the interrupt controller,which clears the corresponding bit in isr.Note that after eoi but before iret,if interrupts are enabled(IF =1),the handler could be interrupted by interrupts at a lower or the same level. Overview of uC/OS-II.uC/OS-II is a commercial preemptive real-time multi- tasking OS kernel developed by Micrium [2].The kernel has 6000+lines of C code and 300+lines of assembly.It allows a fixed number of tasks,multi-levelA Practical Verification Framework for Preemptive OS Kernels 61 Fifth, we also specify and verify priority inversion freedom (PIF) of μC/OS-II. PIF is a crucial property for real-time systems and is worth veri￾fying in its own right. Moreover, since the specification and verification are done at the level of the abstract model (i.e., specifications) of the kernel, they also help validate our model of system APIs. As we explain above, many important properties cannot be specified if the model is too weak or overly abstract. Coq proofs and a companion technical report are available at http://staff. ustc.edu.cn/∼fuming/research/certiucos. 2 Background and Overview of Our Work 2.1 Preemptive OS Kernels and Interrupts In a preemptive OS kernel, execution of a task inside the kernel can be inter￾rupted at any program point (unless interrupts are disabled). Then the control is switched to the interrupt handler. When the handler finishes, it may invoke the scheduler and switch the execution context to a different task, instead of return￾ing to the original interrupted task. For instance, with priority-based scheduling, the interrupt handler always switches to the highest priority task at its end. The x86 Interrupt Mechanism. Interrupt handling and management are indis￾pensable in preemptive OS kernels. We give an overview of the interrupt mech￾anism in x86 systems (based on the Intel 8259 A interrupt controller). The CPU has a flag bit IF indicating whether interrupts are enabled or not. The cli/sti instruction clears/sets the bit to disable/enable interrupts. In 8259 A there is a register isr, each bit of which corresponds to a hardware interrupt and records if the interrupt is being served or not. Different priority levels are assigned to different sources of interrupts, with level-0 being the highest. When an interrupt request comes, we check IF and isr. If the interrupts are enabled and there is currently no interrupt with higher or the same priority being served, the request will be served. The corresponding bit in isr is set to 1 and the control jumps to the corresponding interrupt handler. On the invocations of an interrupt handler, the CPU flags (including IF) are saved on the stack, and interrupts are disabled automatically. If interrupts are enabled again inside the handler, the handler could be further interrupted by requests with higher priorities, causing nested interrupts. The handler returns to the program being interrupted using the iret instruc￾tion, which also restores the flags (including IF). Before the handler returns, it needs to execute eoi to send an “end of interrupt” signal to the interrupt controller, which clears the corresponding bit in isr. Note that after eoi but before iret, if interrupts are enabled (IF = 1), the handler could be interrupted by interrupts at a lower or the same level. Overview of μC/OS-II. μC/OS-II is a commercial preemptive real-time multi￾tasking OS kernel developed by Micrium [2]. The kernel has 6000+ lines of C code and 300+ lines of assembly. It allows a fixed number of tasks, multi-level