[Zurück]

J. Knoop, L. Kovacs, J. Zwirchmayr:
"An Evaluation of WCET Analysis using Symbolic Loop Bounds (abstract/presentation)";
Vortrag: 16. Kolloquium Programmiersprachen und Grundlagen der Programmierung, Schloss Raesfeld, Münsterland, Deutschland; 26.09.2011 - 28.09.2011; in: "Tagungsband 16. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'11)", Westfälische Wilhelms-Universität Münster, 132 (2011), S. 200.

The spread of safety critical real time systems results in an increased necessity for worst case execution time
(WCET) analysis of these systems: finding the time limit within which the software system responds in all
possible scenarios. Computing the WCET for programs with loops or recursion is, in general, undecidable.
We present an automatic method for computing tight upper bounds on the iteration number of special
classes of program loops. These upper bounds are further used in the WCET analysis of programs. The
technique deploys pattern-based recurrence solving in conjunction with program flow refinement using
SMT reasoning. To do so, we refine program flows using SMT reasoning and rewrite certain multi-path
loops into single-path ones, possibly over-approximating the loop-bound. The multi-path loops we consider
are I) abruptly-terminating loops that might terminate early due to break statements and II) loops with
additional monotonic updates, that conditionally modify the loop counter. For those, the minimum increase
of the loop counter is computed and used as loop step expression. Single-path loops are further translated
into a set of recurrence relations over program variables. For solving recurrences we deploy a pattern-
based recurrence solving algorithm, computing closed forms for a restricted class of recurrence equations.
Finally, iteration bounds are derived for program loops from the computed closed forms. We only compute
closed forms for a restricted class of loops, however, in practice, these recurrences describe the behavior
of a large set of program loops that are relevant to WCET analysis. Our technique is implemented in the
r-TuBound tool and was successfully tried out on a number of challenging WCET benchmarks: we evaluate
the symbolic loop bound generation technique and present an experimental evaluation of the method carried
out with the r-TuBound software tool. We evaluate our method against various academic and industrial
WCET benchmarks, and compare the results to the original TuBound tool.

wcet, loop bounds, smt, program analysis

http://publik.tuwien.ac.at/files/PubDat_205571.pdf