Safe and Precise WCET Determination by Abstract Interpretation of Pipeline Models

Abstract

Failure of computer software in a hard real-time system leads to severe consequences and must be avoided by proving the correctness of the systems software. A prerequisite for this is the determination of an upper bound for the worst-case execution times (WCET) of the tasks in the system. We show that for modern CPUs, WCETs can be obtained by static program analysis methods even for CPUs with execution history sensitives components like caches and pipelines. This is the first time that complex CPU features (out-of-order execution, speculation, etc) have been included in a comprehensive and safe analysis. The approach presented in this thesis is able to handle the analysis of very complex architectures (PowerPC 755) by first modeling the CPU and peripherals of the system and then using abstractions on some components of the system to obtain an analysis. The analysis computes WCET for the basic blocks of the program by simulating the abstract system model. The correctness of the approach is shown. A tool has been built based on this approach, which was evaluated under reallife industry conditions by Airbus France in the course of the DAEDALUS project, showing the practical applicability of the methodology.

Fehlverhalten der Computersoftware eines harten Echtzeitsystems kann katastrophale Folgen haben. Um ein solches Verhalten zu verhindern, muss die Korrektheit der Programme des Systems vorher nachgewiesen werden. Eine Voraussetzung hierf®ur ist die Kenntniss von oberen Schranken f®ur die Ausf®uhrungszeit der Programme (WCET). F®ur moderne CPUs k®onnen solche Schranken effektiv nur durch statische Analysemethoden verl®asslich gewonnen werden, da die Laufzeiten stark von kontextsensitiven Komponenten (Caches, Pipelines) abh®angen. Bisher galten komplexe Merkmale moderner CPUs (out-of-order Ausf®uhrung, Spekulation) als nicht efzient statisch analysierbar. Die vorliegende Arbeit pr®asentiert einen Ansatz, der in der Lage ist, sehr komplexe Architekturen (etwa den PowerPC 755) zu behandeln. Hierbei wird zuerst ein Modell des Prozessors und der Peripherie des Systems erstellt, dessen Komponenten dann geeignet abstrahiert werden k®onnen, um eine Analyse zu erhalten. Die Analyse berechnet WCET f®ur die Basisbl®ocke eines Programmes durch Simulation des abstrahierten Prozessormodells. Die Korrektheit der Analyse wird durch die Verwendung der Theorie der abstrakten Interpretation garantiert. Mit diesem Ansatz wurde ein Werkzeug entwickelt, welches unter Industriebedingungen von Airbus France im Verlauf des DAEDALUS Projektes evaluiert wurde. Dabei konnte die praktische Anwendbarkeit des vorgestellten Ansatzes klar demonstriert werden.