Loop Analysis with oRange
Marianne de Michiel and Armelle Bonenfant
Université Paul Sabatier, Toulouse, France
One of the important steps in processing the worst case
execution time (WCET) of a program is to determine the loops upper
bounds. Such bounds are crucial when verifying real-time systems. We
will present oRange, our tool which performs a static loop bound
analysis associating flow analysis and abstract interpretation. It
considers binary operators (+, -, *, /) for the loop increment, nested
loops, non-recursive function calls, simple loop conditions (==, !=,
<, <=, >, >=, &&) and loop upper bound values (instead of
intervals). We will present the different steps of the analysis and
some results on the Mälardalen benchmark suite.
Biographies:
The research interests of the TRACES team include hardware issues of
real-time embedded systems. The main goal is to guarantee that the
execution time of an application code meets the system deadlines. We
focus on characterizing the temporal properties of components
off-the-shelves. Our target is to propose ways to use these components
such that safe and tight worst-case execution time estimates can be
computed. We also study architectural extensions that should improve
the time predictability of the components. The estimation of the WCET
requires three steps: a static analysis of the code identifies all the
possible execution paths; the target hardware is modelled to determine
the individual execution times of the basic blocks; then, the results
of the previous steps are combined to evaluate an upper bound of the
global execution time. Part of our work concerns the first and second
steps.
Marianne de Michiel is an assistant professor, she works especially on
loop bounds. Armelle Bonenfant joined the team in 2007 and
collaborates with Marianne de Michiel.
Contact Armelle and Marianne at:
Ass.-Prof. Armelle Bonenfant
Ass.-Prof. Marianne de Michiel
Institut de Recherche en Informatique de Toulouse (IRIT)
Université Paul Sabatier
118 Route de Narbonne
F-31062 Toulouse, France
ballabri at irit.fr
http://www.irit.fr/recherches/ARCHI/MARCH/index.php3