A Practical verification Framework for Preemptive os Kernels Fengwei Xu Ming Fu Xinyu Feng Xiaoran Zhang Hui zhang Zhaohui Li University of Science and Technology of China Jy22,2016CAV2016 http://staff.ustcedu.cn/-fuming/research/certiucos/
A Practical Verification Framework for Preemptive OS Kernels Fengwei Xu Ming Fu Xinyu Feng Xiaoran Zhang Hui Zhang Zhaohui Li University of Science and Technology of China July 22, 2016 CAV2016 http://staff.ustc.edu.cn/~fuming/research/certiucos/
Motivation of os verification Computer System
Motivation of OS Verification Computer System
Motivation of os verification Applications Operating System Hardware Correctness of OS is crucial for safety and security of the whole system
Motivation of OS Verification Hardware Operating System Applications Correctness of OS is crucial for safety and security of the whole system
Challenges of os Verification Many challenges AsSembly code Concurrency Preemption Interrupts Large code base Device&v/o Concurrency caused by preemptions is particularly challenging
Challenges of OS Verification Many challenges: Preemption … Concurrency C/Assembly code Interrupts Large code base Device & I/O Concurrency caused by preemptions is particularly challenging
Preemption Preemption is the act of temporarily inter nested multi-level t requiring its cooperation interrupts Hand ler 1 Handler 0) Task A Kernel-Level iret preemption cli switch preempt Task B Handler 1 Handler 1 cli switch iret iret s switch iret Preemptions and multi-level interrupts are indispensable to achieve real-time guarantees in rtos Preemptive os kernel is highly concurrent and complex
Preemption Preemptions and multi-level interrupts are indispensable to achieve real-time guarantees in RTOS. Preemptive OS kernel is highly concurrent and complex. . . . . . . cli . . . switch . . . sti . . . Task A . . . sti Handler 1 iret. . . Handler 0 . . . . . . cli . . . switch . . . sti . . . Task B . . . cli . . . switch . . . iret . . . sti . . . eoi Handler 1 . . . iret iret. . . Handler 1 Kernel-Level preemption Preemption is the act of temporarily interrupting a task without requiring its cooperation. nested multi-level interrupts