Document Open Access Logo

Improving WCET Evaluation using Linear Relation Analysis

Authors Pascal Raymond , Claire Maiza , Catherine Parent-Vigouroux , Erwan Jahier , Nicolas Halbwachs , Fabienne Carrier, Mihail Asavoae, Rémy Boutonnet

PDF
Thumbnail PDF

File

LITES-v006-i001-a002.pdf
  • Filesize: 0.77 MB
  • 28 pages

Document Identifiers

Author Details

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

Cite AsGet BibTex

Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Erwan Jahier, Nicolas Halbwachs, Fabienne Carrier, Mihail Asavoae, and Rémy Boutonnet. Improving WCET Evaluation using Linear Relation Analysis. In LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1, pp. 02:1-02:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Real-time systems software
Keywords
  • Worst Case Execution Time estimation
  • Infeasible Execution Paths
  • Abstract Interpretation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  5. Clément Ballabriga, Hugues Cassé, Christine Rochange, and Pascal Sainrat.OTAWA: An open toolbox for adaptive WCET analysis. In SEUS, 2010. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  14. Denis Gopan and Thomas Reps.Lookahead widening. In CAV'06, Seattle, 2006. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  19. Julien Henry, David Monniaux, and Matthieu Moy.PAGAI: A Path Sensitive Static Analyser. Electr. Notes Theor. Comput. Sci., 289:15-25, 2012. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact