A general approach for expressing infeasibility in implicit path enumeration technique - IMAG
Conference Papers Year : 2014

A general approach for expressing infeasibility in implicit path enumeration technique

Pascal Raymond

Abstract

Static timing analysis aims at computing a guaranteed upper bound to the Worst-Case Execution Time (WCET) of a program. It requires both an accurate modeling of the hardware, and a precise analysis of the program in order to reject infeasible executions (in particular, all infinite ones). For the actual computation of the worst-case execution, most of the existing tools and methods are based on the Implicit Path Enumeration Technique (IPET), which consist in encoding this search into a numerical optimization problem (Integer Linear Programming, ILP). An interest of this approach is that it naturally integrates the loop bounds. It also allows to implicitly prune infeasible paths, as far as they can be expressed using linear constraints. Several works on the subject are using this ability in order to enhance the WCET estimation: they identify specific property patterns (e.g., implications, exclusions) and propose ad hoc translation into numerical constraints.

The goal of this paper is to go further than ad hoc reasoning by proposing a general method for translating infeasibility in terms of numerical constraints. It does not address the problem of finding infeasible paths, only the one of characterizing them as precisely as possible. Moreover the paper aims at exploring the limits of the method, and thus, it does not try to enhance the result using additional methods (e.g., graph transformation).

Fichier principal
Vignette du fichier
raymond-ipet14.pdf (381.06 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-04680351 , version 1 (28-08-2024)

Identifiers

Cite

Pascal Raymond. A general approach for expressing infeasibility in implicit path enumeration technique. ESWEEK'14: TENTH EMBEDDED SYSTEM WEEK, Oct 2014, New Delhi India, France. pp.1-9, ⟨10.1145/2656045.2656046⟩. ⟨hal-04680351⟩
24 View
5 Download

Altmetric

Share

More