Ownership-based order reduction and simulation in shared-memory concurrent computer systems

Abstract

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.