Symbolic Worst-Case Execution Time Evaluation with Global Contexts – Sywext

Hard real-time safety critical systems are systems whose correctness depends not only upon the correctness of the produced results, but also on the time at which they are produced. These systems are represented as a set of concurrent tasks, subject to timing constraints. In order to guarantee the respect of timing constraints, a Worst-Case Execution Time (WCET) analysis is performed. WCET computation by static analysis yields an over-approximated upper bound of the maximum running time of the task. While WCET is usually computed as a constant value, we believe that it is beneficial to compute a symbolic WCET, expressed as a formula depending on parameters.

Traditional WCET analysis employs either the IPET method, which is hard to perform parametrically, or (much less frequently) tree-based approaches, which suffer from imprecision and requires the source code. Despite the shortcomings of existing tree-based analyses, we believe they are more suitable to parametric computation. Our objective is to address these shortcomings, and design a precise binary-only tree-based parametric approach that is sufficiently powerful to express a wide range of hardware and software facts, while retaining a tractable analysis complexity.

We partly addressed the shortcomings of tree-based approaches in previous works, where we proposed a tree-based timing model and its analysis for symbolic WCET evaluation. This tree-based model represents two type of properties: 1) structural properties, represented by the tree structure, which express the set of structurally feasible execution paths; 2) non-structural properties, represented by context annotations, which remove execution paths that are structurally feasible, but not semantically feasible.

These previous works are promising, but they are preliminary results : context annotations are limited to local contexts, which is sufficient to represent some limited properties. However, some important properties cannot be represented, because they require to relate some separate elements of the analyzed program, that is to say to handle global contexts. The objective of the Sywext project is to generalize our previous approach
so as to support global contexts. This is an ambitious goal because it requires devising a model that has sufficient expressivity to represent facts provided by a wide range of analyses, while providing a precise timing analysis for this model that keeps a low computational complexity.

Traditional WCET computation is preceded by what we call "auxiliary analyses", that determine timing informations related to the hardware (cache, pipeline, etc.) and software (loop bounds, infeasible paths, etc.). The results of these auxiliary analyses will need to be represented in the tree-model. We will begin the project by surveying auxiliary analyses, defining a global context annotation framework, and expressing the results of auxiliary analyses in our annotation formalism.

Next, we will design a way to evaluate our tree-model with annotations. This will include WCET-preserving tree transformations that simplify the model computation, and heuristics to discard less-important information in order to alleviate the analysis complexity.

We will evaluate our results against traditional WCET analysis on a variety of realistic real-time benchmarks, and compare relevant criteria such as analysis time, and WCET precision.

The project will lead to the development of an opensource analysis tool, and the results will be published in real-time journals and conferences.