Abstract
In the standard framework for worst-case execution time (WCET) analysis of programs, the main data structure is a single instance of integer linear programming (ILP) that represents the whole program. The instance of this NP-hard problem must be solved to find an estimate for WCET, and it must be refined if the estimate is not tight. We propose a new framework for WCET analysis, based on abstract segment trees (ASTs) as the main data structure. The ASTs have two advantages. First, they allow computing WCET by solving a number of independent small ILP instances. Second, ASTs store more expressive constraints, thus enabling a more efficient and precise refinement procedure. In order to realize our framework algorithmically, we develop an algorithm for WCET estimation on ASTs, and we develop an interpolation-based counterexample-guided refinement scheme for ASTs. Furthermore, we extend our framework to obtain parametric estimates of WCET. We experimentally evaluate our approach on a set of examples from WCET benchmark suites and linear-algebra packages. We show that our analysis, with comparable effort, provides WCET estimates that in many cases significantly improve those computed by existing tools.
This research was supported in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), the Austrian National Research Network RiSE (FWF grants S11402-N23), the Swedish VR grant D0497701, the WWTF PROSEED grant ICT C-050, the French National Research Agency grant W-SEPT (ANR-12-INSE-0001), NSF Expeditions award CCF 1138996, DARPA under agreement FA8750-14-2-0263, and a gift from the Intel Corporation.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Altmeyer, S., Humbert, C., Lisper, B., Wilhelm, R.: Parametric timing analysis for complex architectures. In: RTCSA 2008, pp. 367–376 (2008)
Ballabriga, C., Cassé, H., Rochange, C., Sainrat, P.: OTAWA: An Open Toolbox for Adaptive WCET Analysis. In: Min, S.L., Pettit, R., Puschner, P., Ungerer, T. (eds.) SEUS 2010. LNCS, vol. 6399, pp. 35–46. Springer, Heidelberg (2010)
Blackham, B., Liffiton, M., Heiser, G.: Trickle: automated infeasible path detection using all minimal unsatisfiable subsets. In: RTAS, pp. 169–178 (2014)
Bygde, S., Ermedahl, A., Lisper, B.: An efficient algorithm for parametric WCET calculation. Journal of Systems Architecture 57(6), 614–624 (2011)
Bygde, S., Lisper, B.: Towards an Automatic Parametric WCET Analysis. In: Proc. of WCET (2008)
Černý, P., Henzinger, T., Radhakrishna, A.: Quantitative Abstraction Refinement. In: Proc. of POPL, pp. 115–128 (2013)
Chu, D., Jaffar, J.: Symbolic simulation on complicated loops for WCET path analysis. In: EMSOFT, pp. 319–328 (2011)
Cousot, P., Cousot, R.: An abstract interpretation framework for termination. In: Proc. of POPL, pp. 245–258 (2012)
Gulwani, S., Zuleger, F.: The reachability-bound problem. In: Proc. of PLDI, pp. 292–304 (2010)
Huber, B., Prokesch, D., Puschner, P.: A Formal Framework for Precise Parametric WCET Formulas. In: Proc. of WCET, pp. 91–102 (2012)
Huynh, B.K., Ju, L., Roychoudhury, A.: Scope-aware data cache analysis for WCET estimation. In: RTAS 2011, pp. 203–212. IEEE (2011)
Kirner, R.: The WCET Analysis Tool CalcWcet167. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 158–172. Springer, Heidelberg (2012)
Knoop, J., Kovács, L., Zwirchmayr, J.: r-TuBound: Loop Bounds for WCET Analysis (Tool Paper). In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 435–444. Springer, Heidelberg (2012)
Knoop, J., Kovács, L., Zwirchmayr, J.: WCET squeezing: on-demand feasibility refinement for proven precise WCET-bounds. In: RTNS, pp. 161–170 (2013)
Li, Y., Malik, S.: Performance analysis of embedded software using implicit path enumeration. In: DAC, pp. 456–461 (1995)
Puschner, P., Schedl, A.: Computing Maximum Task Execution Times – A Graph-Based Approach. Real-Time Systems 13(1), 67–91 (1997)
Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying loop invariant generation using splitter predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 703–719. Springer, Heidelberg (2011)
Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenström, P.: The Worst-Case Execution-Time Problem - Overview of Methods and Survey of Tools. ACM Trans. Embedded Comput. Syst. 7(3) (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Černý, P., Henzinger, T.A., Kovács, L., Radhakrishna, A., Zwirchmayr, J. (2015). Segment Abstraction for Worst-Case Execution Time Analysis. In: Vitek, J. (eds) Programming Languages and Systems. ESOP 2015. Lecture Notes in Computer Science(), vol 9032. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46669-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-662-46669-8_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46668-1
Online ISBN: 978-3-662-46669-8
eBook Packages: Computer ScienceComputer Science (R0)