Vol. 6 No. 1 (2019)
Regular Papers

Improving WCET Evaluation using Linear Relation Analysis

PDF
  • Pascal Raymond,
  • Claire Maiza,
  • Catherine Parent-Vigouroux,
  • Erwan Jahier,
  • Nicolas Halbwachs,
  • Fabienne Carrier,
  • Mihail Asavoae,
  • Rémy Boutonnet
Pascal Raymond
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAG, Grenoble, France
Claire Maiza
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAG, Grenoble, France
Catherine Parent-Vigouroux
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAG, Grenoble, France
Erwan Jahier
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAG, Grenoble, France
Nicolas Halbwachs
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAG, Grenoble, France
Fabienne Carrier
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAG, Grenoble, France
Mihail Asavoae
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAG, Grenoble, France
Rémy Boutonnet
Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAG, Grenoble, France
Cover LITES Vol.6 Iss.1 2019

Published 2019-02-18

Keywords

  • Worst Case Execution Time estimation,
  • Infeasible Execution Paths,
  • Abstract Interpretation

Copyright (c) 2018 Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Erwan Jahier, Nicolas Halbwachs, Fabienne Carrier, Mihail Asavoae, and Rémy Boutonnet

Creative Commons License

This work is licensed under a Creative Commons Attribution 3.0 Unported License.

How to Cite

[1]
2019. Improving WCET Evaluation using Linear Relation Analysis. Leibniz Transactions on Embedded Systems. 6, 1 (Feb. 2019), 02:1–02:28. DOI:https://doi.org/10.4230/LITES-v006-i001-a002.

Abstract

The precision of a worst case execution time (WCET) evaluation tool on a given program is highly dependent on how the tool is able to detect and discard semantically infeasible executions of the program. In this paper, we propose to use the classical abstract interpretation-based method of linear relation analysis to discover and exploit relations between execution paths. For this purpose, we add auxiliary variables (counters) to the program to trace its execution paths. The results are easily incorporated in the classical workflow of a WCET evaluator, when the evaluator is based on the popular implicit path enumeration technique. We use existing tools - a WCET evaluator and a linear relation analyzer - to build and experiment a prototype implementation of this idea.
PDF

References

  1. Mihail Asavoae, Claire Maiza, and Pascal Raymond.Program Semantics in Model-Based WCET Analysis: A State of the Art Perspective. In 13th International Workshop on Worst-Case Execution Time Analysis, WCET 2013, July 9, 2013, Paris, France, volume 30 of OASICS, pages 32-41. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013.
  2. Roberto Bagnara, Elisa Ricci, Enea Zaffanella, and Patricia M. Hill.Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library. In M. V. Hermenegildo and G. Puebla, editors, 9th International Symposium on Static Analysis, SAS'02, Madrid, Spain, September 2002. LNCS 2477. URL: http://dx.doi.org/10.1007/3-540-45789-5_17
  3. Gogul Balakrishnan and Thomas W. Reps.DIVINE:DIscovering variables IN executables. In Verification, Model Checking, and Abstract Interpretation, VMCAI 2007, pages 1-28, Nice, France, January 2007.
  4. Gogul Balakrishnan, Thomas W. Reps, David Melski, and Tim Teitelbaum.WYSINWYX: what you see is not what you execute. In Verified Software: Theories, Tools, Experiments, VSTTE 2005, pages 202-213, Zurich, Switzerland, October 2005.
  5. Clément Ballabriga, Hugues Cassé, Christine Rochange, and Pascal Sainrat.OTAWA: An open toolbox for adaptive WCET analysis. In SEUS, 2010.
  6. Duc-Hiep Chu, Joxan Jaffar, and Rasool Maghareh.Precise Cache Timing Analysis via Symbolic Execution. In 2016 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pages 1-12, 2016.
  7. Patrick Cousot and Radia Cousot.Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages, POPL'77, Los Angeles, January 1977.
  8. Patrick Cousot and Nicolas Halbwachs.Automatic discovery of linear restraints among variables of a program. In 5th ACM Symposium on Principles of Programming Languages, POPL'78, Tucson (Arizona), January 1978.
  9. Marianne de Michiel, Armelle Bonenfant, Hugues Cassé, and Pascal Sainrat.Static loop bound analysis of C programs based on flow analysis and abstract interpretation. In IEEE Int'l Conf. on Embedded and Real-Time Computing Systems and Applications (RTCSA), 2008.
  10. Sun Ding, Hee Beng Kuan Tan, and Kaiping Liu.A Survey of Infeasible Path Detection. In Proceedings of the 7th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2012), Wroclaw, Poland, 29-30 June, 2012., pages 43-52, 2012.
  11. Heiko Falk, Sebastian Altmeyer, Peter Hellinckx, Björn Lisper, Wolfgang Puffitsch, Christine Rochange, Martin Schoeberl, Rasmus Bo Sorensen, Peter Wägemann, and Simon Wegener.TACLeBench: A Benchmark Collection to Support Worst-Case Execution Time Research. In 16th International Workshop on Worst-Case Execution Time Analysis, WCET 2016, July 5, 2016, Toulouse, France, pages 2:1-2:10, 2016.
  12. Paul Feautrier and Laure Gonnord.Accelerated Invariant Generation for C Programs with Aspic and C2fsm. In Tools for Automatic Program AnalysiS (TAPAS), Perpignan, France, September 2010.
  13. Christian Ferdinand, Florian Martin, Christoph Cullmann, Marc Schlickling, Ingmar Stein, Stephan Thesing, and Reinhold Heckmann.New Developments in WCET Analysis. In Program Analysis and Compilation, pages 12-52, 2006.
  14. Denis Gopan and Thomas Reps.Lookahead widening. In CAV'06, Seattle, 2006.
  15. Jan Gustafsson, Adam Betts, Andreas Ermedahl, and Björn Lisper.The Mälardalen WCET Benchmarks: Past, Present And Future. In Proc. of WCET, pages 136-146, 2010.
  16. Jan Gustafsson, Andreas Ermedahl, Christer Sandberg, and Björn Lisper.Automatic Derivation of Loop Bounds and Infeasible Paths for WCET Analysis Using Abstract Execution. In RTSS, 2006.
  17. Nicolas Halbwachs, Yann-Eric Proy, and Patrick Roumanoff.Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157-185, August 1997.
  18. Julien Henry, Mihail Asavoae, David Monniaux, and Claire Maiza.How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. In SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2014, LCTES '14, pages 43-52, June 2014.
  19. Julien Henry, David Monniaux, and Matthieu Moy.PAGAI: A Path Sensitive Static Analyser. Electr. Notes Theor. Comput. Sci., 289:15-25, 2012.
  20. François Irigoin, Pierre Jouvelot, and Rémy Triolet.Semantical Interprocedural parallelization: An overview of the PIPS Project. In ACM Int. Conf. on Supercomputing, ICS'91, Köln, 1991.
  21. Bertrand Jeannet and Antoine Miné.Apron: A Library of Numerical Abstract Domains for Static Analysis. In Computer Aided Verification (CAV 2009), Grenoble, France, pages 661-667, June 2009.
  22. Raimund Kirner, Peter Puschner, and Adrian Prantl.Transforming flow information during code optimization for timing analysis. Journal on Real-Time Systems, 45(1-2), 2010.
  23. Jens Knoop, Laura Kovács, and Jakob Zwirchmayr.WCET squeezing: on-demand feasibility refinement for proven precise WCET-bounds. In Proceedings of the 21st International Conference on Real-Time Networks and Systems, pages 161-170. ACM, 2013.
  24. Chris Lattner and Vikram Adve.LLVM: a compilation framework fopr lifelong program analysis & transformation. In CGO'04, pages 75-86, Washington, DC, August 2004. IEEE Computer Society.
  25. Hanbing Li, Isabelle Puaut, and Erven Rohou.Traceability of Flow Information: Reconciling Compiler Optimizations and WCET Estimation. In 22nd International Conference on Real-Time Networks and Systems, RTNS'14, Versailles, France, October 8-10, 2014, 2014.
  26. Hanbing Li, Isabelle Puaut, and Erven Rohou.Tracing Flow Information for Tighter WCET Estimation: Application to Vectorization. In 21st IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, page 10, Hong-Kong, China, August 2015. URL: https://hal.inria.fr/hal-01177902.
  27. Xianfeng Li, Liang Yun, Tulika Mitra, and Abhik Roychoudhury.Chronos: A timing analyzer for embedded software. Sci. Comput. Program., 69(1-3):56-67, 2007.
  28. Yau-Tsun Steven Li and Sharad Malik.Performance analysis of embedded software using implicit path enumeration. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 16(12), 1997.
  29. Björn Lisper. SWEET – a tool for WCET flow analysis. In 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA), October 2014.
  30. Paul Lokuciejewski, Daniel Cordes, Heiko Falk, and Peter Marwedel.A Fast and Precise Static Loop Analysis Based on Abstract Interpretation, Program Slicing and Polytope Models. In Proceedings of the CGO 2009, The Seventh International Symposium on Code Generation and Optimization, pages 136-146, Seattle, Washington, USA, March 2009.
  31. Paul Lokuciejewski and Peter Marwedel.Worst-Case Execution Time Aware Compilation Techniques for Real-Time Systems. Springer, 2011. URL: http://dx.doi.org/10.1007/978-90-481-9929-7
  32. Ravindra Metta, Martin Becker, Prasad Bokil, Samarjit Chakraborty, and R. Venkatesh.TIC: a scalable model checking based approach to WCET estimation. In Proceedings of the 17th ACMSIGPLAN/SIGBED Conference on Languages, Compilers, Tools, and Theory for Embedded Systems, LCTES 2016, Santa Barbara, CA, USA, June 13 - 14, 2016, pages 72-81, 2016. URL: http://dx.doi.org/10.1145/2907950.2907961
  33. Antoine Miné.The Octagon Abstract Domain. In Proceedings of the Eighth Working Conference on Reverse Engineering, WCRE'01, Stuttgart, Germany, October 2-5, 2001, page 310, 2001. URL: http://dx.doi.org/10.1109/WCRE.2001.957836
  34. George C. Necula, Scott McPeak, Shree P. Rahul, and Westley Weimer.CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In R. Nigel Horspool, editor, Compiler Construction, pages 213-228, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg.
  35. Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Fabienne Carrier, and Mihail Asavoae.Timing analysis enhancement for synchronous program. Real-Time Systems, pages 1-29, 2015.
  36. Jordy Ruiz and Hugues Cassé.Using SMT Solving for the Lookup of Infeasible Paths in Binary Programs (regular paper). In Workshop on Worst-Case Execution Time Analysis, Lund, Sweden, 07/07/2015, pages 95-104. OASICs, Dagstuhl Publishing, July 2015.
  37. Thomas Sewell, Felix Kam, and Gernot Heiser.Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis. In 2016 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April 11-14, 2016, pages 185-195, 2016. URL: http://dx.doi.org/10.1109/RTAS.2016.7461326
  38. Björn Lisper Stefan Bygde, Andreas Ermedahl.An Efficient Algorithm for Parametric WCET Calculation. Journal of Systems Architecture, 57(6):614-624, May 2011.
  39. Vivy Suhendra, Tulika Mitra, Abhik Roychoudhury, and Ting Chen.Efficient detection and exploitation of infeasible paths for software timing analysis. In DAC, pages 358-363, 2006.
  40. Stephan Thesing, Jean Souyris, Reinhold Heckmann, Famantanantsoa Randimbivololona, Marc Langenbach, Reinhard Wilhelm, and Christian Ferdinand.An Abstract Interpretation-Based Timing Validation of Hard Real-Time Avionics Software. In DSN, pages 625-632, 2003.
  41. Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, Frank Mueller, Isabelle Puaut, Peter Puschner, Jan Staschulat, and Per Stenström.The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst. (TECS), 7(3), 2008.
  42. Jakob Zwirchmayr, Armelle Bonenfant, Marianne de Michiel, Hugues Cassé, Laura Kovács, and Jens Knoop.FFX: A portable WCET annotation language (regular paper). In International Conference on Real-Time and Network Systems (RTNS), Pont-à-Mousson, 08/11/2012-09/11/2012, pages 91-100, November 2012.
  43. Jakob Zwirchmayr, Pascal Sotin, Armelle Bonenfant, Denis Claraz, and Philippe Cuenot.Identifying Relevant Parameters to Improve WCET Analysis (regular paper). In Workshop on Worst-Case Execution Time Analysis, Madrid, 08/07/2014, pages 91-100. OASICs, Dagstuhl Publishing, July 2014.