Provably sound semantics stack for multi-core system programming with kernel threads

Abstract

Operating systems and hypervisors (e.g., Microsoft Hyper-V) for multi-core processor architectures are usually implemented in high-level stack-based programming languages integrated with mechanisms for the multi-threaded task execution as well as the access to low-level hardware features. Guaranteeing the functional correctness of such systems is considered to be a challenge in the field of formal verification because it requires a sound concurrent computational model comprising programming semantics and steps of specific hardware components visible for the system programmer. In this doctoral thesis we address the aforementioned issue and present a provably sound concurrent model of kernel threads executing C code mixed with assembly, and basic thread operations (i.e., creation, switch, exit, etc.), needed for the thread management in OS and hypervisor kernels running on industrial-like multi-core machines. For the justification of the model, we establish a semantics stack, where on its bottom the multi-core instruction set architecture performing arbitrarily interleaved steps executes binary code of guests/processes being virtualized and the compiled source code of the kernel linked with a library implementing the threads. After extending an existing general theory for concurrent system simulation and by utilising the order reduction of steps under certain safety conditions, we apply the sequential compiler correctness for the concurrent mixed programming semantics, connect the adjacent layers of the model stack, show the required properties transfer between them, and provide a paper-and-pencil proof of the correctness for the kernel threads implementation with lock protected operations and the efficient thread switch based on the stack substitution.

Betriebssysteme und Hypervisoren (z.B. Microsofts Hyper-V) für Mehrkernprozessor-Architekturen sind üblicherweise in stapelbasierten höheren Programmiersprachen implementiert, welche integrierte Mechanismen für die mehrfadige Aufgabenausführung sowie den Zugriff auf niedrige Hardwarefunktionen hat. Die funktionale Korrektheit solcher Systeme zu garantieren wird im Gebiet der formalen Verifikation als Herausforderung angesehen, da sie eine korrektes nebenläufiges Berechnungsmodell benötigt, welches die Programmiersprachensemantik ebenso beinhaltet wie die für Systemprogrammierer sichtbaren Schritte der einzelnen Hardwarekomponenten. In dieser Dissertation gehen wir die eben genannten Probleme an und präsentieren ein beweisbar korrektes, nebenläufiges Modell von Betriebssystemkernfaden, die gemischten C- und Assemblerkode ausführen, sowie grundlegenden Fadenoperationen (d.h. Erstellung, Wechsel, Stopp, usw.), die für die Fadenverwaltung in Kernen der Betriebssysteme und Hypervisoren, welchhe auf praxisnahen Mehrkernprozessoren laufen sollen, nötig sind. Für die Rechtfertigung des Modells richten wir einen semantischen Stapel ein, dessen niedrigste Ebene die Mehrkernprozessorarchitektur ist, die beliebig verschränkte Schritte des Binärkodes von virtualisierten Gästen bzw. Prozessen und den kompilierten Quelltext des Kerns, verlinkt mit einer Bibliothek, welche die Faden implementiert, ausführt. Nach wir eine bereits vorhandene allgemeine Theorie für die Simulation nebenläufiger Systeme erweitern und indem wir die Reihenfolgen-Reduktion von Schritten unter bestimmten Sicherheitsbedingungen verwenden, verbinden wir die benachbarten Ebenen des Modellstapels, zeigen die nötigen Eigenschaftsübertragungen zwischen ihnen, und geben einen Papier-und-Bleistift-Beweis für die Korrektheit der Implementierung der Kernfäden mit durch Sperren geschützten Operationen und einem effizienten Fadenwechsel, welcher auf Stapelsubstitution basiert.