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

Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.