Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26653
Titel: Store buffer reduction theorem and application
Verfasser: Chen, Geng
Sprache: Englisch
Erscheinungsjahr: 2016
SWD-Schlagwörter: Speichermodell
Verifikation
ISA
Simulation
Concurrent C
Freie Schlagwörter: weak memory model
sequential consistency
TSO
MMU
formal verification
programming disciplilne
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: The functional correctness of multicore systems can be shown through pervasive formal verification, which proves the simulation between the system software computation and the corresponding hardware computation. In the implementation of the system software, the sequential consistency (SC) of memory is usually assumed by the system programmers. However, most modern processors (x86, Sparc) provide the total store order (TSO) memory model for greater effciency. A store buffer reduction theorem was presented by Cohen and Schirmer to bridge the gap between the SC and the TSO. Nevertheless, the theorem is not applicable to programs that edit their own page tables. The reason is that the MMU can be treated neither as a part of the program thread nor as a separate thread. This thesis contributes to generalize the Cohen-Schirmer reduction theorem by adding the MMUs. As the first contribution of this thesis, we present a programming discipline which guarantees sequential consistency for the TSO machine with MMUs. Under this programming discipline, we prove the store buffer reduction theorem with MMUs. For the second contribution of this thesis, we apply the theorem to the ISA level and the C level. By proving a series of simulation theorems, we apply our store buffer reduction theorem with MMU to the ISA named MIPS-86. After that, we introduce the multicore compiler correctness theorem to map the programming discipline to the parallel C level.
Die funktionale Korrektheit von Mehrkern-Systemen kann durch durchgängige formale Verifikation sichergestellt werden, in welcher die Simulation zwischen Berechnungen der Systemsoftware und der entsprechenden Hardwareberechnungen bewiesen wird. Für die Implementierung der Systemsoftware wird vom Systemprogrammierer im Normalfall das Berechnungsmodell der Sequentiellen Konsistenz (SC) zugrundegelegt. Die meisten modernen Prozessoren (x86, Sparc) bieten jedoch aus Effzienzgründen stattdessen das Berechnungsmodell der Totalen-Schreibzugriff-Ordnung (TSO) an. Cohen und Schirmer präsentieren ein Schreibpufferreduktionstheorem, welches die Lücke zwischen SC und TSO schließt. Dieses Theorem kann allerdings nicht auf Programme angewendet werden, die ihre eigenen Seitentabellen bearbeiten. Der Grund dafür ist, dass die Speicherverwaltungseinkeit (SVE) weder als Teil des Programmfadens noch als separater Faden behandelt werden kann. Diese Dissertation liefert einen Beitrag zur Verallgemeinerung des Cohen-Schirmer Reduktionstheorems, in dem die SVE hinzugenommen wird. Als ersten Beitrag dieser Dissertation präsentieren wir eine Programmierdisziplin welche Sequentielle Konsistenz auf einer TSO Maschine mit SVE garantiert. Unter dieser Programmierdisziplin beweisen wir das Schreibpufferreduktionstheorem mit SVE. Als zweiten Beitrag dieser Dissertation wenden wir das Theorem auf der Ebene der Befehlssatzarchitektur und der C Ebene an. Durch eine Reihe von Simulationstheoremen wenden wir unser Schreibpufferreduktionstheorem mit SVE auf die Befehlssatzarchitektur MIPS-86 an. Danach führen wir ein Mehrkern-Compiler Korrektheitstheorem ein, welches die Programmierdisziplin auf die Ebene von parallelem C abbildet.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-65265
hdl:20.500.11880/26709
http://dx.doi.org/10.22028/D291-26653
Erstgutachter: Paul, Wolfgang J.
Tag der mündlichen Prüfung: 11-Mai-2016
SciDok-Publikation: 23-Mai-2016
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
diss.pdf1,81 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.