Interrupts in OS code: let’s reason about them. Yes, this means concurrency.

Existing modelled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where it runs the flight control software of a high-assurance quadcopter. To provide low latency, the eChronos OS runs with interrupts enabled and provides a preemptive scheduler. In terms of verification, this means that concurrency reasoning is required, which significantly increases the complexity: application and OS instructions may be interleaved with interrupt handler instructions.

In our work we explicitly model the effect of interrupts and their handling by the hardware and OS. We provide a general formal model of the interleaving between OS code, application code and interrupt handlers. We then instantiate this model to formalise the scheduling behavior of the eChronos OS, and prove the main scheduler property: the running task is always the highest-priority runnable task.

June Andronick is a Senior Researcher at Data61|CSIRO (formerly NICTA). Her research focuses on increasing the reliability of critical software systems, by mathematically proving that the code behaves as expected and satisfies security and safety requirements.  She contributed to the seL4 correctness proof and now focuses on concurrency reasoning for OS code. She leads the concurrency software verification research in Data61, and is deputy leader of the Trustworthy Systems group. She was recognised in 2011 by MIT's Technology Review as one of the world's top young innovators (TR35). She holds a PhD in Computer Science from the University of Paris-Sud, France.