Symbolic Computation of the Worst-Case Execution Time of a Program

TL;DR

This paper introduces a new symbolic computation method for parametric worst-case execution time analysis of programs, offering advantages over ILP-based approaches in efficiency and accuracy.

Contribution

The paper presents a novel symbolic computation approach for parametric WCET analysis, avoiding ILP and improving efficiency and result quality.

Findings

Our method dominates existing parametric analysis techniques.

Results are comparable to ILP-based approaches in accuracy.

The approach maintains good computational efficiency.

Abstract

Parametric Worst-case execution time (WCET) analysis of a sequential program produces a formula that represents the worst-case execution time of the program, where parameters of the formula are user-defined parameters of the program (as loop bounds, values of inputs or internal variables, etc). In this paper we propose a novel methodology to compute the parametric WCET of a program. Unlike other algorithms in the literature, our method is not based on Integer Linear Programming (ILP). Instead, we follow an approach based on the notion of symbolic computation of WCET formulae. After explaining our methodology and proving its correctness, we present a set of experiments to compare our method against the state of the art. We show that our approach dominates other parametric analyses, and produces results that are very close to those produced by non-parametric ILP-based approaches, while keeping very good computing time.