Name
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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-43144-4_4 | INTERACTIVE THEOREM PROVING (ITP 2016) |
Field | DocType | Volume |
HOL,Interrupt,Programming language,Concurrency control,Scheduling (computing),Computer science,Concurrency,Hoare logic,Algorithm,System call,Context switch,Distributed computing | Conference | 9807 |
ISSN | Citations | PageRank |
0302-9743 | 3 | 0.47 |
References | Authors | |
10 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| June Andronick | 1 | 903 | 42.66 |
| Corey Lewis | 2 | 33 | 3.30 |
| Daniel Matichuk | 3 | 129 | 6.01 |
| C. C. Morgan | 4 | 1462 | 174.73 |
| Christine Rizkallah | 5 | 75 | 14.05 |