Safe and precise WCET determination by abstract interpretation of pipeline models [Elektronische Ressource] / von Stephan Thesing
265 Pages
English
Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

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

Downloading requires you to have access to the YouScribe library
Learn all about the services we offer
265 Pages
English

Description

Safe and Precise WCETDetermination by AbstractInterpretation of Pipeline ModelsDissertationzur Erlangung des Grades eines Doktors derIngenieurwissenschaften (Dr.-Ing.) derNaturwissenschaftlich-Technischen Fakultaten¤ derUniversitat¤ des SaarlandesvonDiplom-InformatikerStephan ThesingSaarbruck¤ enJuli 2004Tag des Kolloquiums: 18.11.2004Dekan: Prof. Dr. Jor¤ g Eschmeier, Universitat¤ des SaarlandesPrufungsausschuss:¤Vorsitzender Prof. Dr. Holger Hermanns, Universitat¤ des SaarlandesGutachter: Prof. Dr. Reinhard Wilhelm, Universitat¤ desProf. Dr. Werner Damm, Universitat¤ OldenburgAkad. Mitarbeiter: Dr. Christian Lindig, Universitat¤ des SaarlandesiErklarung¤Hiermit versichere ich an Eides statt, dass ich die vorliegende Arbeit selbststandig¤und ohne Benutzung anderer als der angegebenen Hilfmittel angefertigt habe. Dieaus anderen Quellen oder indirekt ubernommenen¤ Daten und Konzepte sind unterAngabe 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, deniiShort AbstractFailure 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-caseexecution times (WCET) of the tasks in the system.

Subjects

Informations

Published by
Published 01 January 2005
Reads 8
Language English
Document size 1 MB

Exrait

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. This approach is being studied in the AVACS
Transregional Collaborative Research Center 14 sponsored by the German Re-
search Foundation DFG. More processors (Motorola PPC 5xx, In neon Tricore,
Ti TMS320C33, Motorola STAR12) have been or are being modeled in this frame-
work at the moment by the company AbsInt.
viZusammenfassung
Als harte Echtzeitsyteme bezeichnet man allgemein Computersysteme, welche
kritische physikalische Umgebungen kontrollieren (etwa Flugzeugsteuerungen,
Atomkraftwerkssteuerungen, Waffenlenksysteme, etc). Falls ein solches Comput-
ersystem Fehler aufweist, konnen¤ die Konsequenzen drastisch sein: Hohe Sach-
schaden¤ oder sogar Verlust von Menschenleben. Daher mussen¤ harte Echtzeit-
systeme vor dem Einsatz auf ihre Korrektheit uberpr¤ uft¤ werden. Ein Aspekt der
Korrektheit ist die rechtzeitige Antwort des Systems, die oft durch Zeitschranken
angegeben wird, die von den Tasks im Computersystem eingehalten werden mus-¤
sen. Ein wesentlicher Bestandteil des Nachweises, dass jede Task ihre Zeitschran-
ke einhalt¤ ist die Kenntniss der Ausfuhrungszeit¤ der Task im schlimmsten Fall,
ihrer worst-case execution time (WCET). Es hat sich meist als nicht praktikabel
heraus gestellt, die WCET durch Messen realer Ausfuhrungszeiten¤ zu bestimmen,
da komplexe Abhangigk¤ eiten zwischen der Ausfuhrungszeit¤ und den Eingabe-
daten oder Startzustanden¤ des Systems bestehen. Daher konnen¤ sichere obere
Schranken fur¤ die WCET nur durch Benutzung statischer Analysemethoden auf
dem Programmcode erhalten werden. Da die Formen der in harten Echtzeit-
systemen benutzten Programmierstile eingeschrankt¤ sind (keine Benutzung von
Zeigern, kein Heap, beschrankte¤ Rekursion, etc), ist es prinzipiell moglich,¤ eine
WCET allein vom Programmcode her zu berechnen (bekannte Schleifendurch-
lauf- und Rekursionsschranken).
Moderne CPUs benutzen Verfahren, etwa Caches und Pipelines, zur Erhohung¤
ihrer Performanz. Diese Verfahren konnen¤ zu einer hohen Varianz der Ausfuhr-¤
ungszeit fuhren,¤ da sie von der Ausfuhrungsgeschichte¤ abhangen:¤ Ein Speicherzu-
griff z.B. kann lediglich einen Takt in Anspruch nehmen, wenn er ein Cachetre-
ffer ist, oder er kann uber¤ 50 Takte dauern, wenn das gewunschte¤ Datum nicht
im Cache liegt und aus dem Hauptspeicher geholt werden muss. Ob ein Zugriff
ein Cachetreffer ist hangt¤ von dem Cacheinhalt und daher von den vor diesem
¤Zugriff ausgefuhrten¤ Zugriffen ab. Ahnliches gilt fur¤ die Effekte innerhalb der
Prozessorpipeline. Die statische Analyse solcher Eigenschaften heutiger CPUs
hat sich als schwierig erwiesen. Bis vor kurzem wurde die Analyse von CPUs mit
Sprungvorhersage, out-of-order Ausfuhrung¤ oder Spekulation als zu komplex fur¤
den praktischen Einsatz angesehen, vgl. [Eng02].
Wir stellen einen neuen Ansatz vor, der in der Lage ist, Architekturen mit
den oben genannten Eigenschaften fur¤ realistische Programme zu analysieren.
Unser Ansatz basiert auf einem Modell der CPU und der Peripherie (Speicher,
System Controller). Wir benutzen ein zyklengenaues Modell mit untereinander
kommuniziernden Einheiten, welche einen inneren Zustand aufweisen und mit
Zustandsuber¤ gangsregeln ausgestattet sind. Dies lehnt sich an Ansatze¤ aus dem
Gebiet der Hardwarebeschreibungssprachen an, etwa VHDL oder Verilog. Im An-
viischluss an die Modellierung werden mit Hilfe der Theorie der abstrakten Interpre-
tation (sichere) Abstraktionen fur¤ einige der Komponenten des Modells de niert,
die das Modell auf die fur¤ das Zeitverhalten wichtige Bestandteile reduzieren und
die Grosse¤ des Modells auf ein handhabbares Ma s bringen. Wenn die durch-
gefuhrten¤ Abstraktionen gewisse, aus der Theorie der abstrakten Interpretation
stammende, Bedingungen erfullen,¤ ist garantiert, dass jeder konkrete Modellzu-
stand von einem abstrakten Zustand reprasentiert¤ wird, d.h. die Abstraktionen
sind sicher. Das durch diesen Prozess erhaltene abstrakte Modell kann immer
noch zyklenweise simuliert werden, wodurch man sichere obere Schranken fur¤ die
Ausfuhrungszeit¤ der Basisblock¤ e des Programms bekommt. Pipelineeffekte wer-
den zusatzlich¤ uber¤ Basisblockgrenzen hinweg propagiert. Die WCETs fur¤ die
Basisblock¤ e, zusammen mit dem Kontroll ussgraphen des Programmes konnen¤
dann in ein ganzzahlig-lineares Programm uberf¤ uhrt¤ werden, wobei die Gesam-
tausfuhrungzeit¤ des Programmes als zu maximierende Zielfunktion formuliert
wird. Eine Losung¤ dieses Programmes ist dann eine sichere obere Schranke fur¤
die Ausfuhrungszeit¤ des Programmes. Diese Arbeit prasentiert¤ zwei detaillierte
Modelle fur¤ den Motorola ColdFire 5307 und den Motorola PowerPC 755 zusam-
men mit den zur Erlangung des abstrakten Modells durchgefuhrten¤ Abstraktionen.
Die abstrakte Simulation wird dann als Transferfunktion einer Daten ussanalyse
(DFA) uber¤ dem Kontroll ussgraphen des Programmes benutzt. Diese DFA ist
dann der Kern der Implementierung der WCET Analyse des Programmes.
Dieser Ansatz hat zur Entwicklung eines kommerziellen Werkzeuges, aiT,
gefuhrt,¤ welches auf beweisbar korrekten Grundlagen basiert und in der Lage ist,
komplexe Architekturen zur Berechnung von WCETs realistischer Programme zu
behandeln. Seine Prototypen wurden wahrend¤ des DAEDALUS Projektes durch
Airbus France mit realistischen Benchmarks fur¤ Avionics Software unter indus-
triellen Bedingungen evaluiert. Das Werkzeug erhielt einen IST Preis der Eu-
ropaischen¤ Union. Dies zeigt die praktische Relevanz und Anwendbarkeit des
vorgestellten Ansatzes.
Andere, fur¤ die reale Anwendbarkeit von WCET Werkzeugen wichtige As-
pekte werden ebenfalls diskutiert: Validierung von WCET W und Vorher-
sagbarkeit von Hardware. Die V der von Werkzeugen geliefer-
ten Ergebnisse ist wichtig, wenn sie in einem Bereich wie der Avionic einge-
setzt werden sollen. Da unser Werkzeug auf beweisbar korrekten Abstraktionen
beruht, dient die Validierung hier nur der Absicherung gegen Implementierungs-
fehler und Fehlern im Modell. Vorhersagbare Hardware bezeichnet Hardware,
deren Verhalten im schlimmsten Fall nicht weit entfernt ist vom Verhalten im
durchschnittlichen Fall. Dies macht die Vorhersage von WCETs einfacher und
praziser¤ , da weniger Unfalle ¤ im Verhalten der Hardware modelliert oder kon-
servativ abgeschatzt¤ werden mussen.¤ Die Identi kation problematischer Eigen-
schaften in Prozessoren, welche ein ungunstiges¤ Verhalten im schlimmsten Fall
viiiausweisen, ist daher ein wichtiger Schritt im Entwurf zukunftiger¤ Echtzeitsys-
teme.
Der vorgestellte Ansatz kann in verschiedene Richtungen durch die Benutzung
andere Modellierungstechniken erweitert werden. Z.B. konnte¤ ein VHDL Modell
eines Prozessors durch Abstraktionsschritte auf ein abstraktes Modell reduziert
werden. Diese Erweiterung wird zur Zeit im transregionalen Sonderforschungs-
bereich AVACS der DFG untersucht. Derzeit werden zusatzliche¤ Prozessoren
(Motorola PPC 5xx, In neon Tricore, Ti TMS320C33, Motorola STAR12) im
Rahmen dieses Ansatzes von der Firma AbsInt modelliert.
ix