OASIcs.WCET.2018.8.pdf
- Filesize: 404 kB
- 13 pages
Document
Embedded Program Annotations for WCET Analysis
Authors
-
Part of:
Volume:
18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018)
Series: Open Access Series in Informatics (OASIcs)
Conference: Workshop on Worst-Case Execution Time Analysis (WCET) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-09-24
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
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.
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)
0PDF Downloads
References
-
AbsInt Angewandte Informatik GmbH. a³ for PPC User Documentation (Version 18.04).
- AbsInt Angewandte Informatik GmbH. aiT Worst-Case Execution Time Analyzer. URL: http://www.absint.com/ait/.
- AbsInt Angewandte Informatik GmbH. CompCert: formally verified optimizing C compiler. URL: http://www.absint.com/compcert/.
- AbsInt Angewandte Informatik GmbH. TimeWeaver: Hybrid Worst-Case Timing Analysis. URL: http://www.absint.com/timeweaver/.
- 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.
-
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.
-
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.
- ENTRA Consortium. Deliverable D2.1 "Common Assertion Language". URL: http://entraproject.ruc.dk/deliverables.
- 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.
-
Xavier Leroy. A formally verified compiler back-end. J. Automated Reasoning, 43(4):363-446, 2009.
-
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.
- 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.
- 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.
- 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.
- 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.