A Formal Framework for Precise Parametric WCET Formulas
A Formal Framework for Precise Parametric WCET Formulas
复制标题
精确参数 WCET 公式的正式框架
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
P. Puschner
中科院分区：
文献类型：
--
作者：
Benedikt Huber;Daniel Prokesch;P. Puschner
参数最坏情况执行时间(WCET)公式是在设计时估计输入数据属性对WCET的影响或在运行时指导调度决策的有价值的工具。以前的参数WCET分析方法要么只提供非正式的特别解决方案，要么倾向于相当悲观，因为它们没有考虑简单循环界限以外的流约束。我们围绕路径和频率表达式开发了一个形式化的框架，它允许我们推理程序部分的执行频率。从一个可约的控制流图和一组(参数)约束出发，我们展示了如何获得频率表达式并通过声音近似来细化它们，这解释了
更复杂的流量约束。最后，我们通过部分求值的方法得到了封闭形式的参数WCET公式。我们开发了一个原型，实现了我们的参数WCET分析解决方案，并在我们的环境中比较了现有的方法。作为我们的框架
支持细粒度转换以提高参数公式的精度，它允许专注于重要的流关系，以避免难以处理的大公式。
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.