Verifikation quantitativer Eigenschaften eines Mikrokernbetriebssystems durch eine Kombination von probabilistischem Model Checking und interaktivem Theorembeweisen
Final Report Abstract
Für die Konstruktion moderner Mikrokerne sind systematische Methoden für den Nachweis zentraler funktionaler und quantitativer Eigenschaften unerlässlich. Der Schwerpunkt des Projekts QuaOS lag auf dem Einsatz von probabilistischem Model Checking als formale Analysemethode für den Nachweis quantitativer Eigenschaften, wie etwa die Aussage, dass für einen erfolgreichen Zugriff auf eine Sperrvariable mit einer Wahrscheinlichkeit von 1—10^-6 nicht mehr als drei Versuche benötigt werden oder dass die Reaktionszeit auf eine anstehende Unterbrechung in 98% aller Fälle höchstens 2 μs beträgt. Solche Eigenschaften stehen in engem Zusammenhang mit der Optimierung von Mikrokernen. So rechtfertigt z.B. die zuerst genannte quantitative Anforderung die Verwendung hochperformanter, jedoch unfairer Locks. Die Verwendung von weichen Echtzeitbedingungen, wie mit der zweitgenannten Eigenschaft angedeutet, ist sinnvoll in Umgebungen, in denen im Mittel eine hohe Dienstgüte unbedingt sichergestellt werden muss, jedoch das gelegentliche Nichteinhalten der Dienstgüte hinnehmbar ist. Ein Beispielen hierfür ist die Dekodierung eines Videodatenstroms. Sowohl die Konstruktion geeigneter mathematischen Modelle als auch die Analyse des Modells hinsichtlich quantitativer Eigenschaften stellen wissenschaftliche Herausforderungen dar. Im Verlauf des Projekts haben wir ausführliche Fallstudien mit einem Spinlockprotokoll als repräsentatives Beispiel durchgeführt, um das Auffinden geeigneter stochastischer Verteilungen durch eine Kombination von Messungen und probabilistischem Model Checking zu illustrieren. Auf diese Weise konnte eine stochastische Modellierung komplexer Cacheeffekte gefunden werden, die für kleine Prozessanzahl einen fast perfekten Abgleich zwischen messbasierten Analyseergebnissen und den durch einen probabilistischem Model Checking berechneten Ergebnissen ermöglichte. Anhand dieses Modells wurde probabilistisches Model Checking eingesetzt, um Vorhersagen für das quantitative Verhalten des Spinlockprotokolls für eine große Anzahl an Prozessen und die Skalierbarkeit von probabilistischem Model Checking unter Einsatz verschiedener Techniken zur Behandlung des Problems der Zustandsexplosion zu untersuchen. Eine zweite umfangreiche Fallstudie untersuchte das Potential eines lockfreien Ressourcenmanagementprotokolls, das den inhärenten Probabilismus moderner High Performance Computer zur Symmetriebrechung auszunutzen versucht. Die Durchführung der Fallstudien deckte einige Unzulänglichkeiten von state-of-the-art probabilistischen Model Checkern auf und führte zu der Erkenntnis, dass einige für die Bewertung von Betriebssystemprotokollen relevante quantitive Maße bislang noch nicht oder kaum im Bereich formaler Methoden adressiert wurden. In unseren aktuellen Arbeiten haben wir hierfür entsprechende Berechnungsalgorithmen und prototypische Implementierungen entworfen, die wir in Folgeprojekten weiterentwickeln werden.
Publications
- Chiefly symmetric; Results on the scalability of probabilistic model checking for operating-system code. In 7th Conference on Systems Software Verification (SSV), volume 102 of Electronic Proceedings in Theoretical Computer Science, pages 156-166, 2012
Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews, and Marcus Völp
- Waiting for locks: How long does it usually take? In 17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), volume 7437 of Lecture Notes in Computer Science, pages 47-62. Springer, 2012
Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews, and Marcus Völp
- A probabilistic quantitative analysis of probabilistic-write/copy-select. In NASA Formal Methods (NFM), volume 7871 of Lecture Notes in Computer Science, pages 307-321. Springer, 2013
Christel Baier, Benjamin Engel, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews, and Marcus Völp
- Computing quantiles in Markov reward models. In 16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 7794 of Lecture Notes in Computer Science, pages 353-368. Springer, 2013
Michael Ummels and Christel Baier
- Formalizing cut elimination of coalgebraic logics in Coq. In 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), volume 8123 of Lecture Notes in Artificial Intelligence, pages 257-272. Springer, 2013
Hendrik Tews
- Locks: Picking key methods for a scalable quantitative analysis. Journal of Computer and System Sciences 81(1):258–287 • February 2015
Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews, and Marcus Völp
(See online at https://doi.org/10.1016/j.jcss.2014.06.004)
