Document Open Access Logo

WCET of OCaml Bytecode on Microcontrollers: An Automated Method and Its Formalisation

Authors Steven Varoumas, Tristan Crolard

PDF
Thumbnail PDF

File

OASIcs.WCET.2019.5.pdf
  • Filesize: 0.56 MB
  • 12 pages

Document Identifiers

Author Details

Steven Varoumas
  • Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, F-75005, Paris, France
  • Cnam, Centre d'études et de recherche en informatique et communications, Cédric, 292 rue Saint Martin, 75003, Paris, France
Tristan Crolard
  • Cnam, Centre d'études et de recherche en informatique et communications, Cédric, 292 rue Saint Martin, 75003, Paris, France

Cite AsGet BibTex

Steven Varoumas and Tristan Crolard. WCET of OCaml Bytecode on Microcontrollers: An Automated Method and Its Formalisation. In 19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019). Open Access Series in Informatics (OASIcs), Volume 72, pp. 5:1-5:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/OASIcs.WCET.2019.5

Abstract

Considering the bytecode representation of a program written in a high-level programming language enables portability of its execution as well as a factorisation of various possible analyses of this program. In this article, we present a method for computing the worst-case execution time (WCET) of an embedded bytecode program fit to run on a microcontroller. Due to the simple memory model of such a device, this automated WCET computation relies only on a control-flow analysis of the program, and can be adapted to multiple models of microcontrollers. This method evaluates the bytecode program using concrete as well as partially unknown values, in order to estimate its longest execution time. We present a software tool, based on this method, that computes the WCET of a synchronous embedded OCaml program. One key contribution of this article is a mechanically checked formalisation of the aforementioned method over an idealised bytecode language, as well as its proof of correctness.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Embedded software
  • Computer systems organization → Real-time systems
Keywords
  • Worst-case execution time
  • microcontrollers
  • synchronous programming
  • bytecode
  • OCaml

Metrics

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

Supplementary Materials

References

  1. Clément Ballabriga, Julien Forget, and Giuseppe Lipari. Symbolic WCET computation. ACM Transactions on Embedded Computing Systems (TECS), 17(2):39, 2018. URL: http://dx.doi.org/10.1145/3147413.
  2. Guillem Bernat, Alan Burns, and Andy J. Wellings. Portable worst-case execution time analysis using Java Byte Code. In Proceedings of the 12th Euromicro Conference on Real-Time Systems (ECRTS 2000), Stockholm, Sweden, June 19-21, 2000, pages 81-88, New York, NY, USA, 2000. IEEE. URL: http://dx.doi.org/10.1109/EMRTS.2000.853995.
  3. Niels Brouwers, Koen Langendoen, and Peter Corke. Darjeeling, a Feature-rich VM for the Resource Poor. In Proceedings of the 7th International Conference on Embedded Networked Sensor Systems (SenSys 2009), Berkeley, CA, USA, November 4-6, 2009, pages 169-182, New York, NY, USA, 2009. ACM. URL: http://dx.doi.org/10.1145/1644038.1644056.
  4. Paul Caspi, Daniel Pilaud, Nicolas Halbwachs, and John Plaice. Lustre: A Declarative Language for Programming Synchronous Systems. In Proceedings of the 14th annual ACM Symposium on Principles of Programming Languages (POPL 1987), Munich, Germany, January 21-23, 1987, pages 178-188, New York, NY, USA, 1987. ACM. URL: http://dx.doi.org/10.1145/41625.41641.
  5. Franck Cassez, René Rydhof Hansen, and Mads Chr. Olesen. What is a Timing Anomaly? In Proceedings of the 12th International Workshop on Worst-Case Execution Time Analysis (WCET 2012), Pisa, Italy, July 10, 2012, volume 23 of OpenAccess Series in Informatics (OASIcs), pages 1-12, Dagstuhl, Germany, 2012. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/OASIcs.WCET.2012.1.
  6. Marc Feeley and Danny Dubé. PICBIT: A Scheme system for the PIC microcontroller. In Proceedings of the 4th Workshop on Scheme and Functional Programming, Boston, MA, USA, pages 7-15, 2003. URL: http://www.schemeworkshop.org/2003.
  7. Fei Guan, Long Peng, Luc Perneel, and Martin Timmerman. Open Source FreeRTOS As a Case Study in Real-time Operating System Evolution. Journal of Systems and Software, 118(C):19-35, August 2016. URL: http://dx.doi.org/10.1016/j.jss.2016.04.063.
  8. William Hallahan, Anton Xue, and Ruzica Piskac. Building a Symbolic Execution Engine for Haskell. In Proceedings of the 8th Workshop on Tools for Automatic Program Analysis (TAPAS 2017), New York, NY, USA, August 29, 2017, 2017. URL: https://cs.nyu.edu/acsys/tapas2017.
  9. Trevor Harmon and Raymond Klefstad. A Survey of Worst-Case Execution Time Analysis for Real-Time Java. In Proceedings of the 21th International Parallel and Distributed Processing Symposium (IPDPS 2007), 26-30 March 2007, Long Beach, CA, USA, pages 1-8. IEEE, 2007. URL: http://dx.doi.org/10.1109/IPDPS.2007.370422.
  10. Niklas Holsti and Sam Saarinen. Status of the Bound-T WCET tool. In Proceedings of the 2nd International Workshop on Worst-Case Execution Time Analysis (WCET 2002), Technical University of Vienna, Austria, June 2002. URL: http://www.cs.york.ac.uk/rts/wcet2002.
  11. Xavier Leroy. The ZINC experiment: an economical implementation of the ML language. Technical Report 117, INRIA, 1990. URL: https://hal.inria.fr/inria-00070049/file/RT-0117.pdf.
  12. André Oliveira Maroneze, Sandrine Blazy, David Pichardie, and Isabelle Puaut. A Formally Verified WCET Estimation Tool. In Proceedings of the 14th International Workshop on Worst-Case Execution Time Analysis (WCET 2014), Ulm, Germany, July 8, 2014, volume 39 of OpenAccess Series in Informatics (OASIcs), pages 11-20, Dagstuhl, Germany, 2014. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/OASIcs.WCET.2014.11.
  13. Corina S. Pasareanu and Neha Rungta. Symbolic PathFinder: symbolic execution of Java bytecode. In Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010), Antwerp, Belgium, September 20-24, 2010, pages 179-180, New York, NY, USA, 2010. ACM. URL: http://dx.doi.org/10.1145/1858996.1859035.
  14. Peter P. Puschner and Christian Koza. Calculating the Maximum Execution Time of Real-Time Programs. Real-Time Systems, 1(2):159-176, 1989. URL: http://dx.doi.org/10.1007/BF00571421.
  15. Jan Reineke, Björn Wachter, Stefan Thesing, Reinhard Wilhelm, Ilia Polian, Jochen Eisinger, and Bernd Becker. A Definition and Classification of Timing Anomalies. In Proceedings of the 6th International Workshop on Worst-Case Execution Time Analysis (WCET '06), Dresden, Germany, July 4, 2006, volume 4 of OpenAccess Series in Informatics (OASIcs), Dagstuhl, Germany, 2006. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/OASIcs.WCET.2006.671.
  16. Martin Schoeberl and Rasmus Pedersen. WCET analysis for a Java processor. In Proceedings of the 4th international workshop on Java technologies for real-time and embedded systems (JTRES '06), Paris, France, October 11-13, 2006, pages 202-211, New York, NY, USA, 2006. ACM. URL: http://dx.doi.org/10.1145/1167999.1168033.
  17. Koushik Sen. Concolic testing. In Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007), Atlanta, Georgia, USA, November 5-9, 2007, pages 571-572, New York, NY, USA, 2007. ACM. URL: http://dx.doi.org/10.1145/1321631.1321746.
  18. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, et al. Ott: Effective tool support for the working semanticist. Journal of Functional Programming, 20(1):71-122, 2010. URL: http://dx.doi.org/10.1017/S0956796809990293.
  19. Vincent St-Amour and Marc Feeley. PICOBIT: a compact Scheme system for microcontrollers. In Proceedings of the 21st International Symposium on Implementation and Application of Functional Languages (IFL 2009), South Orange, NJ, USA, September 23-25, 2009, pages 1-17. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-16478-1_1.
  20. The Coq Development Team. The Coq Proof Assistant, version 8.9.0, January 2019. URL: http://dx.doi.org/10.5281/zenodo.2554024.
  21. Steven Varoumas, Benoît Vaugon, and Emmanuel Chailloux. Concurrent Programming of Microcontrollers, a Virtual Machine Approach. In Proceedings of the 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016), Toulouse, France, 2016. URL: https://hal.archives-ouvertes.fr/ERTS2016.
  22. Steven Varoumas, Benoît Vaugon, and Emmanuel Chailloux. OCaLustre : une extension synchrone d'OCaml pour la programmation de microcontrôleurs. In Vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA 2017), Gourette, France, 2017. URL: https://hal.archives-ouvertes.fr/JFLA2017.
  23. Steven Varoumas, Benoît Vaugon, and Emmanuel Chailloux. A Generic Virtual Machine Approach for Programming Microcontrollers: the OMicroB Project. In Proceedings of the 9th European Congress on Embedded Real Time Software and Systems (ERTS 2018), Toulouse, France, 2018. URL: https://hal.archives-ouvertes.fr/ERTS2018.
  24. Benoît Vaugon, Philippe Wang, and Emmanuel Chailloux. Programming Microcontrollers in OCaml: The OCaPIC Project. In Proceedings of the 17th International Symposium on Practical Aspects of Declarative Languages (PADL 2015), Portland, OR, USA, June 18-19, 2015, pages 132-148. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-19686-2_10.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact