Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26559
Titel: Ownership-based order reduction and simulation in shared-memory concurrent computer systems
Sonstige Titel: Ownership-basierte Reihenfolgenreduktion und Simulation in nebenläufigen Computersystemen mit gemeinsamem Speicher
Verfasser: Baumann, Christoph
Sprache: Englisch
Erscheinungsjahr: 2014
SWD-Schlagwörter: Verifikation
Concurrent C
C-Compiler
Makroassembler
Simulation
Nebenläufigkeit
Formale Spezifikationstechnik
Reduktion
Freie Schlagwörter: multicore
memory safety
correctness
pervasive verification
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: The highest level of confidence in the correct functionality of system software can be gained from a pervasive formal verification approach, where the high-level language application layer is connected to the gate-level hardware layer through a stack of semantic layers coupled by simulation theorems. While such semantic stacks exist for sequential systems, the foundational theory of semantic stacks for concurrent systems is still incomplete. This thesis contributes to close this gap. First we prove a general order reduction theorem establishing a model where processes are executing blocks of steps, being only interleaved at selectable interleavingpoints. An ownership-based memory access policy is imposed to prove commutativity properties for non-synchronizing steps, enabling the desired reordering. In contrast to existing work, we only assume properties on the order-reduced level, thus providing a complete abstraction. We then apply sequential simulation theorems on top of the block schedules and prove a general simulation theorem between two abstract concurrent systems including the transfer of safety properties. Finally we instantiate our frameworks with a MIPS instruction set architecture, a macro assembler (MASM) semantics, and an intermediate language semantics for C. Applying the concurrent simulation theorem, we justify the concurrent semantics of MASM and C against their ISA implementation.
Das größte Vertrauen in die korrekte Funktionsweise von System-Software kann mit Hilfe durchdringender formaler Beweisverfahren erlangt werden, welche alle Abstraktionsebenen eines Computersystems durch Simulationstheoreme miteinander koppeln. Während solche Gerüste von Semantiken bereits für sequentielle Systeme entwickelt wurden, finden sich in der entsprechenden Theorie für nebenläufige Systeme noch Lücken, zur Schließung derer diese Arbeit beitragen soll. Zunächst beweisen wir ein allgemeines Reduktionstheorem, das die möglichen Reihenfolgen, in der Prozesse Schritte machen, auf ein Modell beschränkt, in dem Blöcke von Schritten verschiedener Prozesse nacheinander ausgeführt werden. Mittels eines ”Ownership”-basierten Speicherzugriffprotokolls beweisen wir Kommutativitätseigenschaften für lokale Schritte verschiedener Prozesse und ermöglichen so das Vertauschen dieser. Da unser Theorem nur Eigenschaften des reihenfolgereduzierten Systems annimmt ermöglicht es eine vollständige Abstraktion vom ursprünglichen Modell. Auf die Blockausführung wenden wir sequentielle Simulationstheoreme an und beweisen ein allgemeines Simulationstheorem zwischen abstrakten nebenläufigen Systemen sowie den Transfer von Sicherheitseigenschaften. Wir instanziieren das Theorem mit einem MIPS-Instruktionssatz und Semantiken für Makroassembler und C. Dadurch rechtfertigen wir die nebenläufige Semantik der Programmiersprachen gegen ihre Maschinenimplementierung.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-57214
hdl:20.500.11880/26615
http://dx.doi.org/10.22028/D291-26559
Erstgutachter: Paul, Wolfgang J.
Tag der mündlichen Prüfung: 19-Mär-2014
SciDok-Publikation: 27-Mär-2014
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 
Ba14.pdf1,25 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.