Safe and precise WCET determination by abstract interpretation of pipeline models [Elektronische Ressource] / von Stephan Thesing

Sujets

• Informatik

Informations

• Publié par: universitat_des_saarlandes
• Publié le: 01 janvier 2005
• Nombre de lectures: 8
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Safe and Precise WCET
Determination by Abstract
Interpretation of Pipeline Models
Dissertation
zur Erlangung des Grades eines Doktors der
Ingenieurwissenschaften (Dr.-Ing.) der
Naturwissenschaftlich-Technischen Fakultaten¤ der
Universitat¤ des Saarlandes
von
Diplom-Informatiker
Stephan Thesing
Saarbruck¤ en
Juli 2004Tag des Kolloquiums: 18.11.2004
Dekan: Prof. Dr. Jor¤ g Eschmeier, Universitat¤ des Saarlandes
Prufungsausschuss:¤
Vorsitzender Prof. Dr. Holger Hermanns, Universitat¤ des Saarlandes
Gutachter: Prof. Dr. Reinhard Wilhelm, Universitat¤ des
Prof. Dr. Werner Damm, Universitat¤ Oldenburg
Akad. Mitarbeiter: Dr. Christian Lindig, Universitat¤ des Saarlandes
iErklarung¤
Hiermit versichere ich an Eides statt, dass ich die vorliegende Arbeit selbststandig¤
und ohne Benutzung anderer als der angegebenen Hilfmittel angefertigt habe. Die
aus anderen Quellen oder indirekt ubernommenen¤ Daten und Konzepte sind unter
Angabe der Quelle gekennzeichnet.
Die Arbeit wurde bisher wieder im In- noch im Ausland in gleicher oder ahnlicher¤
Form in einem Verfahren zur Erlangung eines akademischen Grades vorgelegt.
Saarbruck¤ en, den
iiShort Abstract
Failure of computer software in a hard real-time system leads to severe conse-
quences and must be avoided by proving the correctness of the system’s 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 rst 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 rst 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 real-
life industry conditions by Airbus France in the course of the DAEDALUS project,
showing the practical applicability of the methodology.
iiiKurze Zusammenfassung
Fehlverhalten der Computersoftware eines harten Echtzeitsystems kann katas-
trophale Folgen haben. Um ein solches Verhalten zu verhindern, muss die Korrek-
theit der Programme des Systems vorher nachgewiesen werden. Eine Vorausset-
zung hierfur¤ ist die Kenntniss von oberen Schranken fur¤ die Ausfuhrungszeit¤ der
Programme (WCET). Fur¤ moderne CPUs konnen¤ solche Schranken effektiv nur
durch statische Analysemethoden verlasslich¤ gewonnen werden, da die Laufzeiten
stark von kontextsensitiven Komponenten (Caches, Pipelines) abhangen.¤ Bisher
galten komplexe Merkmale moderner CPUs (out-of-order Ausfuhrung,¤ Spekula-
tion) als nicht ef zient statisch analysierbar.
Die vorliegende Arbeit prasentiert¤ einen Ansatz, der in der Lage ist, sehr kom-
plexe Architekturen (etwa den PowerPC 755) zu behandeln. Hierbei wird zuerst
ein Modell des Prozessors und der Peripherie des Systems erstellt, dessen Kom-
ponenten dann geeignet abstrahiert werden konnen,¤ um eine Analyse zu erhalten.
Die Analyse berechnet WCET fur¤ die Basisblock¤ e eines Programmes durch Sim-
ulation 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 Indus-
triebedingungen von Airbus France im Verlauf des DAEDALUS Projektes eva-
luiert wurde. Dabei konnte die praktische Anwendbarkeit des vorgestellten An-
satzes klar demonstriert werden.
ivAbstract
Hard real-time systems are computer systems that control critical physical plants
(avionics, automotive, nuclear power plant control, weapon guidance, etc). If
such a computer system fails, the consequences can be severe: damaged prop-
erty or even loss of lifes. Therefore, hard real-time systems must be checked for
correctness before being deployed. One aspect of correctness is the timely re-
sponse of the system, often expressed by temporal deadlines that must be met by
the software tasks in the system. An essential component for proving that every
task meets its deadline is the knowledge of an upper bound for the execution time
of each task, then worst-case execution time (WCET). It has been shown to be
usually practically impossible to obtain the WCET by measuring real execution
times of tasks, due to the complex dependencies between the execution time and
the input data or starting conditions of the system. Thus, safe upper bounds for
the WCET can only be obtained by statically analyzing a task’s program code.
Due to the restricted forms of programming used in hard real-time systems, it is in
principle possible to compute a WCET from the program text alone (loop iteration
and recursion bounds are assumed to be known).
Modern CPUs use features like caches and pipelines to improve performance.
These features can lead to a huge variation in execution time as they are history
sensitive: a memory access, e. g., may take just one cycle for an access that hits
in the cache, while it may take more than 50 cycles for a cache miss and subse-
quent access to main memory. Whether an access hits in the cache depends on the
contents of the cache and thus on the accesses performed before that access. A
similar observation holds for effects in the processor’s pipeline. The static analy-
sis of such features in todays CPUs has proven dif cult. Until recently, the static
analysis of CPUs featuring branch prediction, out-of-order execution or specula-
tion has been viewed as too complex to be used in practice [Eng02].
We present a novel approach that is able to analyze architectures with the be-
fore mentioned features for real-life sized example programs. Our approach is
based on a model of the CPU and the peripherals (memory, system controller,. . . ).
We use a cycle-precise model with communicating units which have inner state
and update rules. This resembles approaches taken by hardware description lan-
guages like VHDL or Verilog. The framework of abstract interpretation is used
to de ne (safe) abstractions for some of the components of the model (e. g. the
caches), reducing the model to details relevant to timing and to a size that can
be practically handled. If the abstractions performed satisfy certain conditions,
following from the theory of abstract interpretation, they are guaranteed to be
safe in the sense that every concrete model state is subsumed by an abstract one.
The abstract model obtained by this process can still be simulated cycle-wise and
its simulation gives safe WCETs of the basic blocks of a program, while taking
vinto account pipeline effects even across basic block boundaries. The WCETs for
the basic blocks together with the control- ow graph of the program can then be
transformed into an integer linear program with the global execution time as the
objective function to be maximized. The solution of this ILP is then a safe WCET
of the program. This work presents two models in detail, namely for the Motorola
ColdFire 5307 and the PowerPC 755, together with the abstractions used to ob-
tain the abstract model for both processors. The abstract model simulation is then
used as the transfer function of a data- ow analysis (DFA) over the control- ow
graph of the binary program to be analyzed. This DFA is then the core of the
implementation of the WCET analysis for the program.
This approach has led to the development of a commercial tool, aiT, which
is based on provably correct methods and able to handle complex architectures
for the computation of WCETs for real-life sized programs. Its prototypes have
been evaluated during the DAEDALUS project by Airbus France with realistic
benchmarks for avionics software under industry conditions. It has been awarded
an European IST award 2004. This demonstrates the practical relevance and ap-
plicability of the approach presented in this thesis.
Other aspects that are of relevance for the real-life utilization of WCET tools
are discussed in this thesis: validation of WCET tools and predictable hardware.
Validating the results of a WCET tool is critical if it is to be deployed in a critical
area like avionics. As our tool is based on provably correct abstractions, vali-
dation serves to detect implementation errors or errors made in the model itself.
Predictable hardware means hardware whose worst-case behavior does not differ
too much from its average-case behavior, making WCET prediction easier and
more precise. The identi cation of problematic features in processors that have
a bad worst-case behavior is thus an important step for design decisions in future
real-time systems.
The approach can be extended in several ways, by using different model-
ing techniques, e. g. a model obtained from the authoritative VHDL code of a
processor by abstraction steps