Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26700
Titel: Provably sound semantics stack for multi-core system programming with kernel threads
Alternativtitel: Der beweisbar korrekte Semantikstapel für Mehrkern-Systemprogrammierung mit Betriebssystemkernfäden
VerfasserIn: Alekhin, Artem
Sprache: Englisch
Erscheinungsjahr: 2016
Kontrollierte Schlagwörter: Thread
Kernel <Informatik>
Mehrkernprozessor
Systemprogrammierung
Verifikation
Freie Schlagwörter: kernel threads
thread switch
system programming
semantics stack
software verification
multi-core
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Dissertation
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.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-67904
hdl:20.500.11880/26756
http://dx.doi.org/10.22028/D291-26700
Erstgutachter: Paul, Wolfgang J.
Tag der mündlichen Prüfung: 24-Feb-2017
Datum des Eintrags: 6-Mär-2017
Fakultät: MI - Fakultät für Mathematik und Informatik
Fachrichtung: MI - Informatik
Sammlung:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Dateien zu diesem Datensatz:
Datei Beschreibung GrößeFormat 
phdthesis_aalekhin.pdf2,65 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.