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.
Type de document :
Article dans une revue
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. 〈http://link.springer.com/article/10.1007%2Fs10817-009-9119-8〉. 〈10.1007/s10817-009-9119-8〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01214588
Contributeur : Burkhart Wolff <>
Soumis le : lundi 12 octobre 2015 - 15:41:01
Dernière modification le : jeudi 11 janvier 2018 - 06:27:34

Identifiants

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. 〈http://link.springer.com/article/10.1007%2Fs10817-009-9119-8〉. 〈10.1007/s10817-009-9119-8〉. 〈hal-01214588〉

Partager

Métriques

Consultations de la notice

41