Skip to Main content Skip to Navigation
Journal articles

Proving Fairness and Implementation Correctness of a Microkernel Scheduler.

Abstract : We report on the formal proof of a microkernel’s key property, namely that its multi-priority process scheduler guarantees progress, i. e., strong fairness. The proof archi- tecture links a layer of behavioral reasoning over system-trace sets with a concrete, fairly realistic implementation written in C. Our microkernel provides an infrastructure for memory virtualization, for communica- tion with hardware devices, for processes (represented as a sequence of assembly instruc- tions, which are executed concurrently over an underlying, formally defined processor), and for inter-process communication (IPC) via synchronous message passing. The kernel es- tablishes process switches according to IPCs and timer-events; the scheduling of process switches, however, follows a hierarchy of priorities, favoring, e. g., system processes over application processes over maintenance processes. Besides the quite substantial models developed in Isabelle/HOL and the formal clar- ification of their relationship, we provide a detailed analysis what formal requirements a microkernel imposes on the key ingredients (hardware, timers, machine-dependent code) in order to establish the correct operation of the overall system. On the methodological side, we show how early modeling with foresight to the later verification has substantially helped our project.
Document type :
Journal articles
Complete list of metadatas

https://hal.inria.fr/hal-01214588
Contributor : Burkhart Wolff <>
Submitted on : Monday, October 12, 2015 - 3:41:01 PM
Last modification on : Wednesday, September 16, 2020 - 5:10:29 PM

Links full text

Identifiers

Collections

Citation

Daum Mathias, Dörrenbächer Jan, Burkhart Wolff. Proving Fairness and Implementation Correctness of a Microkernel Scheduler.. Journal of Automated Reasoning, Springer Verlag, 2009, In: G. Klein, R. Huuck and B. Schlich: Special Issue on Operating System Verification, 42 (2-4), pp.349-388. ⟨10.1007/s10817-009-9119-8⟩. ⟨hal-01214588⟩

Share

Metrics

Record views

161