Document Open Access Logo

Embedded Program Annotations for WCET Analysis

Authors Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, Simon Wegener

PDF

File

Thumbnail PDF
PDF
OASIcs.WCET.2018.8.pdf
  • Filesize: 404 kB
  • 13 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Computer systems organization → Real-time systems
  • Hardware → Static timing analysis
  • Software and its engineering → Embedded software
  • Software and its engineering → Software verification
  • Software and its engineering → Automated static analysis
  • Software and its engineering → Compilers
Keywords
  • Worst-Case Execution Time (WCET) Analysis
  • Annotation Support
  • CompCert
  • Tool Coupling
  • aiT

Metrics

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

Abstract

We present __builtin_ais_annot(), a user-friendly, versatile way to transfer annotations (also known as flow facts) written on the source code level to the machine code level. To do so, we couple two tools often used during the development of safety-critical hard real-time systems, the formally verified C compiler CompCert and the static WCET analyzer aiT. CompCert stores the AIS annotations given via __builtin_ais_annot() in a special section of the ELF binary, which can later be extracted automatically by aiT.

Cite As Get BibTex

Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, and Simon Wegener. Embedded Program Annotations for WCET Analysis. In 18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018). Open Access Series in Informatics (OASIcs), Volume 63, pp. 8:1-8:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/OASIcs.WCET.2018.8

Author Details

Bernhard Schommer
  • Saarland Informatics Campus, Saarland University Building E1.3, D-66123 Saarbrücken, Germany
Christoph Cullmann
  • AbsInt Angewandte Informatik GmbH, Science Park 1, D-66123 Saarbrücken, Germany
Gernot Gebhard
  • AbsInt Angewandte Informatik GmbH, Science Park 1, D-66123 Saarbrücken, Germany
Xavier Leroy
  • INRIA Paris, 2 rue Simone Iff, 75589 Paris, France
Michael Schmidt
  • AbsInt Angewandte Informatik GmbH, Science Park 1, D-66123 Saarbrücken, Germany
Simon Wegener
  • AbsInt Angewandte Informatik GmbH, Science Park 1, D-66123 Saarbrücken, Germany

References

  1. AbsInt Angewandte Informatik GmbH. a³ for PPC User Documentation (Version 18.04). Google Scholar
  2. AbsInt Angewandte Informatik GmbH. aiT Worst-Case Execution Time Analyzer. URL: http://www.absint.com/ait/.
  3. AbsInt Angewandte Informatik GmbH. CompCert: formally verified optimizing C compiler. URL: http://www.absint.com/compcert/.
  4. AbsInt Angewandte Informatik GmbH. TimeWeaver: Hybrid Worst-Case Timing Analysis. URL: http://www.absint.com/timeweaver/.
  5. Philip Axer, Rolf Ernst, Heiko Falk, Alain Girault, Daniel Grund, Nan Guan, Bengt Jonsson, Peter Marwedel, Jan Reineke, Christine Rochange, Maurice Sebastian, Reinhard von Hanxleden, Reinhard Wilhelm, and Wang Yi. Building timing predictable embedded systems. ACM Trans. Embedded Comput. Syst., 13(4):82:1-82:37, 2014. URL: http://dx.doi.org/10.1145/2560033.
  6. Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. Formally verified optimizing compilation in ACG-based flight control software. In ERTS 2012: Embedded Real Time Software and Systems, 2012. Google Scholar
  7. Christoph Cullmann, Christian Ferdinand, Gernot Gebhard, Daniel Grund, Claire Maiza (Burguière), Jan Reineke, Benoît Triquet, Simon Wegener, and Reinhard Wilhelm. Predictability Considerations in the Design of Multi-Core Embedded Systems. Ingenieurs de l'Automobile, 807:26-42, 2010. Google Scholar
  8. ENTRA Consortium. Deliverable D2.1 "Common Assertion Language". URL: http://entraproject.ruc.dk/deliverables.
  9. Heiko Falk and Paul Lokuciejewski. A compiler framework for the reduction of worst-case execution times. Real-Time Systems, 46(2):251-300, 2010. URL: http://dx.doi.org/10.1007/s11241-010-9101-x.
  10. Xavier Leroy. A formally verified compiler back-end. J. Automated Reasoning, 43(4):363-446, 2009. Google Scholar
  11. Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. CompCert - a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 2016. Google Scholar
  12. Hanbing Li, Isabelle Puaut, and Erven Rohou. Traceability of flow information: Reconciling compiler optimizations and WCET estimation. In Mathieu Jan, Belgacem Ben Hedia, Joël Goossens, and Claire Maiza, editors, 22nd International Conference on Real-Time Networks and Systems, RTNS '14, Versaille, France, October 8-10, 2014, page 97. ACM, 2014. URL: http://dx.doi.org/10.1145/2659787.2659805.
  13. Adrian Prantl, Markus Schordan, and Jens Knoop. Tubound - A conceptually new tool for worst-case execution time analysis. In Raimund Kirner, editor, 8th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, Prague, Czech Republic, July 1, 2008, volume 8 of OASICS. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2008. URL: http://dx.doi.org/10.4230/OASIcs.WCET.2008.1661.
  14. Simon Wegener. Towards Multicore WCET Analysis. In Jan Reineke, editor, 17th International Workshop on Worst-Case Execution Time Analysis, WCET 2017, June 27, 2017, Dubrovnik, Croatia, volume 57 of OASICS, pages 7:1-7:12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/OASIcs.WCET.2017.7.
  15. Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David B. Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, Frank Mueller, Isabelle Puaut, Peter P. 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., 7(3):36:1-36:53, 2008. URL: http://dx.doi.org/10.1145/1347375.1347389.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact