Sound semantics of a high-level language with interprocessor interrupts

Abstract

Pervasive formal verification guarantees highest reliability of complex multi-core computer systems. This is required especially for safety critical applications in automotive, medical and military technologies. A crucial part of formal verification is the profound understanding of all system layers and the correct specification of their computational models and the interaction between software and hardware. The underlying architecture and the semantics of the higher-level programs cannot be considered in isolation. In particular, when the program execution relies on specific hardware features, these features have to be integrated into the computational model of the programing language. In this thesis, we present an integration approach for interprocessor interrupts provided by multi-core architectures in the pervasive verification of system software written in C. We define an extension to the semantics of a high-level language, which considers interprocessor interrupts. We prove simulation between a multi-core hardware model and the high-level semantics with interrupts. In this simulation, we assume interrupts to occur on the boundary between statements. We justify that assumption by stating and proving an order reduction theorem, to reorder the interprocessor interrupt service routines to dedicated consistency points.

Formale durchdringende Verifikation garantiert die höchste Zuverlässigkeit von komplexen Multi-Core Computersystemen. Das ist insbesondere bei sicherheitskritischen Anwendungen in der Automobil-, Medizin- und Militärtechnik unerlässlich. Ein wesentlicher Bestandteil der formalen Verifikation ist das tiefgründige Verständnis aller Ebenen des Modell-Stacks und die korrekte Spezifikation deren Rechenmodelle und des Zusammenspiels zwischen Software und Hardware. Die zugrunde liegende Hardwarearchitektur und die Semantik der abstrakten Programmiersprache können nicht isoliert voneinander betrachtet und analysiert werden. Insbesondere dann, wenn sich die Programmausführung auf Eigenschaften der Hardware stützt, müssen diese Eigenschaften in das Rechenmodell der Programmiersprache integriert werden. In dieser Arbeit präsentieren wir einen Integrationsansatz für Inter-Prozessor-Interrupts von Multi-Core-Architekturen in die durchdringende Verifikation der Systemsoftware geschrieben in C. Wir definieren eine Erweiterung der Semantik einer Hochsprache, die Inter-Prozessor-Interrupts berücksichtigt. Wir beweisen Simulation zwischen einem Multi-Core-Hardware-Modell und der High-Level-Semantik mit Interrupts. In dieser Simulation nehmen wir an, dass Interrupts an der Grenze zwischen Anweisungen auftreten. Wir rechtfertigen diese Annahme durch die Definition und den Beweis eines Reduktionstheorem, um die Interprozessor-Interrupt-Service-Routinen zu dedizierten Konsistenz-Punkten zu reordern.