Please use this identifier to cite or link to this item: doi:10.22028/D291-27383
Title: Correctness of multi-core processors with operating system support
Author(s): Lutsyk, Petro
Language: English
Year of Publication: 2018
DDC notations: 004 Computer science, internet
Publikation type: Dissertation
Abstract: Im Zuge der Unterstützung von Hypervisoren verifizieren wir einen realistischen Pipeline-Multi-Core-Prozessor mit integriertem Mechanismus für die zweiphasige (verschachtelte) Adressübersetzung. Das verschachtelte Übersetzungsschema wird benötigt, damit Gäste des Hypervisors (typischerweise Betriebssysteme) ihre Programme im übersetzten Modus ausführen können. Wir betrachten das Setup, in dem die Betriebssysteme als Prozesse (im übersetzten Modus) des Hypervisors laufen, 'auf der bloßen Hardware', d.h. ohne Adressübersetzung. Die geschachtelte Übersetzung wird von der geschachtelten Memory Management Unit (MMU) durchgeführt, wobei beide Übersetzungsphasen in Hardware ausgeführt werden. Sowohl die Spezifikation als auch die Implementierung der geschachtelten MMU werden ausführlich dargestellt. Es wird bewiesen, dass die geschachtelte MMU eine allgemeinere Hilfsspezifikation, die die geschachtelte MMU vom Rest der Maschine isoliert, korrekt implementiert. Letzteres erlaubt es uns, die Argumente für die Korrektheit der MMU-Implementierung in jeder Maschine auf eine einfache Simulation zwischen zwei Softwaremodellen zu reduzieren.Der Hauptbeitrag dieser Arbeit ist der vollständige Korrektheitsbeweis auf Papier für die Pipeline-Multi-Core-Implementierung des MIPS-86 ISA, der zur Unterstützung der verschachtelten Übersetzung zusätzlich erweitert wurde. Wie der Name schon vermuten lässt, kombiniert MIPS-86 den Befehlssatz von MIPS mit dem Speichermodell von x86. Zuerst betrachten wir diese erweiterte MIPS-86-Spezifikation in der sequentiellen Implementierung, die dazu dient, die Integration der verschachtelten MMUs in den MIPS-Prozessor zu demonstrieren und der Einfachheit halber auf einen einzelnen Prozessorkern beschränkt ist. Im Beweis unseres Hauptergebnisses - Korrektheit der Pipeline-Implementierung - verweisen wir auf den sequentiellen Fall, um die Korrektheit der MMU-Operation zu zeigen. Dies erlaubt uns, den Fokus auf die Probleme des Pipelinings der Maschine mit spekulativer Ausführung und Unterbrechungen zu verlagern, die bei vorhandener Adressübersetzung zu berücksichtigen sind.
In the course of adding support for hypervisors, we verify a realistic pipelined multi-core processor with integrated mechanism for two-phase (nested) address translation. The nested translation scheme is required to allow guests of the hypervisor (typically operating systems) to execute their programs in translated mode. We consider the setup in which the operating systems are running as processes (in translated mode) of the hypervisor, running 'on the bare hardware', i.e., without address translation. The nested translation is performed by the nested memory management unit (MMU), with both phases of translation performed in hardware. Both the specification and the implementation of the nested MMU are presented in full detail. The nested MMU is proven to correctly implement an auxiliary, more general specification which isolates the nested MMU from the rest of the machine. The latter allows us to reduce arguments on correctness of the MMU implementation in any machine to a simple simulation between a pair of software models. The main contribution of this thesis is the complete paper and pencil correctness proof for the pipelined multi-core implementation of the MIPS-86 ISA, additionally extended to support the nested translation. As the name suggests, MIPS-86 combines the instruction set of MIPS with the memory model of x86. First, we consider this extended MIPS-86 specification in the sequential implementation, which serves to demonstrate integration of the nested MMUs into the MIPS processor and for simplicity is restricted to have a single processor core. In the proof of our main result - correctness of the pipelined implementation - we refer to the sequential case to show correctness of the MMU operation. This allows us to shift the focus towards the problems of pipelining the machine with speculative execution and interrupts, which are necessary to consider in the presence of address translation.
Link to this record: urn:nbn:de:bsz:291-scidok-ds-273830
hdl:20.500.11880/27182
http://dx.doi.org/10.22028/D291-27383
Advisor: Paul, Wolfgang Jakob
Date of oral examination: 27-Sep-2018
Date of registration: 17-Oct-2018
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
dissertation_lutsyk.pdf1,18 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.