Verifying Preemptive Kernel Code with Preemption Control Support

Kernel preemption is an important feature among mainstream OS kernels. It allows that a kernel thread can be preempted by another kernel thread by performing context switch. A kernel thread can access shared data by disabling kernel preemption temporarily without turning off interruption. Kernel preemption and preemption control reduce kernel response time, but at the same time make kernels more difficult to develop or verify. It is difficult to define their clear semantics and reason about preemptive kernel code. In this paper, we propose a verification framework to verify preemptive kernel code with kernel preemption control. In the framework, we cannot only verify the implementation of preemption control, but also verify the preemptive kernel code which may turn-on/off kernel preemption. The basic idea of the framework is that we build an intermediate abstract layer, where kernel threads, preemption status and interrupt context are made into abstract resources such that we can easily specify the global invariant of the kernel and reason about code with the help of abstract knowledge.