Proof of OS scheduling behavior in the presence of interrupt-induced concurrency

Select |




Print


Andronick, June; Lewis, Corey; Matichuk, Daniel; Morgan, Carroll; Rizkallah, Christine

Andronick, June; Lewis, Corey; Matichuk, Daniel; Morgan, Carroll; Rizkallah, Christine


2016-08-22


Conference Material


Interactive Theorem Proving


Nancy, France


52-68


We present a simple yet scalable framework for formal reasoning and machine-assisted proof of interrupt-driven concurrency in operating-system code, and use it to prove the principal scheduling property of the embedded, real-time eChronos OS : that the running task is always the highest-priority runnable task. The key differentiator of this verification is that the OS code itself runs with interrupts on, even within the scheduler, to minimise latency. Our reasoning includes context switching, interleaving with interrupt handlers and nested interrupts; and it is formalised in Isabelle/HOL, building on the Owicki-Gries method for fine-grained concurrency. We add support for explicit concurrency control and the composition of multiple independently-proven invariants. Finally, we discuss how scalability issues are addressed with proof engineering techniques, in order to handle thousands of proof obligations.


Springer


https://itp2016.inria.fr/


nicta:9261


Andronick, June; Lewis, Corey; Matichuk, Daniel; Morgan, Carroll; Rizkallah, Christine. Proof of OS scheduling behavior in the presence of interrupt-induced concurrency. In: Jasmin Christian Blanchette and Stephan Merz Editor, editor/s. Interactive Theorem Proving; Nancy, France. Springer; 2016-08-22. 52-68.



Loading citation data...

Citation counts
(Requires subscription to view)