Trustworthy Systems

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

Authors

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

Data61
CSIRO

UNSW

Abstract

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.

BibTeX Entry

  @inproceedings{Andronick_LMMR_16,
    address          = {Nancy, France},
    author           = {Andronick, June and Lewis, Corey and Matichuk, Daniel and Morgan, Carroll and Rizkallah, Christine},
    booktitle        = {International Conference on Interactive Theorem Proving},
    editor           = {{Jasmin Christian Blanchette and Stephan Merz}},
    month            = aug,
    pages            = {52--68},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/9261.pdf},
    publisher        = {Springer},
    title            = {Proof of {OS} scheduling behavior in the presence of interrupt-induced concurrency},
    year             = {2016}
  }

Download