[ main page ] [ back ]

25/2012 : A Formal Framework for Precise Parametric WCET Formulas

RR Number
25/2012
Conference
WCET 2012
Author(s)
Benedikt Huber, Daniel Prokesch, Peter Puschner
Abstract
Parametric worst-case execution time (WCET) formulas are a valuable tool to estimate the impact of input data properties on the WCET at design time, or to guide scheduling decisions at runtime. Previous approaches to parametric WCET analysis either provide only informal ad-hoc solutions or tend to be rather pessimistic, as they do not take flow constraints other than simple loop bounds into account. We develop a formal framework around path- and frequency expressions, which allow us to reason about execution frequencies of program parts. Starting from a reducible control flow graph and a set of (parametric) constraints, we show how to obtain frequency expressions and refine them by means of sound approximations, which account for more sophisticated flow constraints. Finally, we obtain closed-form parametric WCET formulas by means of partial evaluation. We developed a prototype, implementing our solution to parametric WCET analysis, and compared existing approaches within our setting. As our framework supports fine-grained transformations to improve the precision of parametric formulas, it allows to focus on important flow relations in order to avoid intractably large formulas.
Bibtex
@InProceedings{huber_et_al:OASIcs:2012:3560,
  author =	{Benedikt Huber and Daniel Prokesch and Peter Puschner},
  title =	{{A Formal Framework for Precise Parametric WCET Formulas}},
  booktitle =	{12th International Workshop on Worst-Case Execution Time Analysis},
  pages =	{91--102},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-41-5},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{23},
  editor =	{Tullio Vardanega},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3560},
  URN =		{urn:nbn:de:0030-drops-35608},
  doi =		{http://dx.doi.org/10.4230/OASIcs.WCET.2012.91},
  annote =	{Keywords: Worst-case execution time analysis, parametric WCET analysis, path expressions, frequency expressions, algebraic framework}
}
Download

[ main page ] [ back ]