Informations générales
Entité de rattachement
Le CEA est un acteur majeur de la recherche, au service des citoyens, de l'économie et de l'Etat.
Il apporte des solutions concrètes à leurs besoins dans quatre domaines principaux : transition énergétique, transition numérique, technologies pour la médecine du futur, défense et sécurité sur un socle de recherche fondamentale. Le CEA s'engage depuis plus de 75 ans au service de la souveraineté scientifique, technologique et industrielle de la France et de l'Europe pour un présent et un avenir mieux maîtrisés et plus sûrs.
Implanté au cœur des territoires équipés de très grandes infrastructures de recherche, le CEA dispose d'un large éventail de partenaires académiques et industriels en France, en Europe et à l'international.
Les 20 000 collaboratrices et collaborateurs du CEA partagent trois valeurs fondamentales :
• La conscience des responsabilités
• La coopération
• La curiosité
Référence
2024-32974
Description de l'unité
The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, development and innovation in four main areas: defense and security, nuclear and renewable energies, technological research for industry, fundamental research in the physical sciences and life sciences. Drawing on its widely acknowledged expertise, the CEA actively participates in collaborative projects with a large number of academic and industrial partners. One of three institutes that comprise CEA Tech, the List institute is committed to technological innovation in digital systems. Within the DSCIN department of CEA List, the LECA laboratory invests R&D efforts in the analysis and verification of timing properties of embedded systems.
http://www-list.cea.fr/
Description du poste
Domaine
Mathématiques, information scientifique, logiciel
Contrat
Stage
Intitulé de l'offre
Benchmarking the scalability of model-checker-based detection of timing anomalies H/F
Sujet de stage
Safety-critical systems such as autonomous vehicles and modern avionic computers have to satisfy strong timing requirements. A failure to meet a timing constraint, missing a deadline for example, may result in serious malfunctions. Therefore, it is crucial to compute safe timing bounds for these systems.
Durée du contrat (en mois)
[3 à 6 mois]
Description de l'offre
Rejoignez-nous en Stage !
Worst-Case Execution Time (WCET) analyses compute sound and (desirably) tight worst-case execution bounds, exploring, via convenient abstractions, all the execution paths of a program running on a computer architecture. This process is complicated by the presence of Timing Anomalies (TA) [1], a counterintuitive behavior in the sense that the local worst-case timing behavior, typically due to a cache miss, does not result in the global worst-case performance. TAs thus require an exhaustive exploration of the reachable hardware states, which is costly or often even prohibitive.
The LECA laboratory has developed a framework to detect TAs [2, 3] within programs, that is based on a formal model of a representative Out-of-Order (OoO) pipeline of processors described using the TLA+ high-level language [4]. The output of the gem5 simulator is used to generate program specifications from input C source codes, and local timing variations are generated using heuristics targeting the latencies of memory instructions. Finally, TA is expressed as an hyper-property in TLA+ and formally verified with the TLC model-checker over a combined formal model of the pipeline and a program.
A first goal of this internship is to evaluate the scalability of this workflow, in particular for identifying the lifetime of TAs but also their patterns. It requires to represent in the formal specification of programs the notion of basic blocks, the atomic analysis unit in static WCET analyses. This will enable to study whether TAs can propagate across several basic blocks and help to capture the limits of the workflow. These evaluations will be performed on an higher number of source codes from the TACLe benchmarks than currently supported. Another goal of this internship is then to study how the scalability of this workflow can be optimized by either using the output of WCET cache analyses to narrow the set of latency variations, vary the verification instant for the detection of TAs or by using different model-checkers, such as the Apalache symbolic model-checker for TLA+ [5].
[1] T. Lundqvist et al., “Timing anomalies in dynamically scheduled microprocessors,” in Real-Time Systems Symposium, 1999.
[2] M. Asavoae et al. Formal executable models for automatic detection of timing anomalies. In: 18th International Workshop on Worst-Case Execution Time Analysis, WCET 2018. pp. 2:1–2:13 (2018).
[3] B. Binder, et al., "Is This Still Normal? Putting Definitions of Timing Anomalies to the Test," 2021 IEEE 27th International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), Houston, TX, USA, 2021, pp. 139-148.
[4] Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc. (2002)
[5] Igor Konnov et al. TLA+ model checking made symbolic. Proc. ACM Program. Lang. 3, OOPSLA, Article 123 (October 2019).
Moyens / Méthodes / Logiciels
Méthodes formelles, micro-architecture, temps réel
Profil du candidat
Computer engineering student (final year) or master 2 student with knowledge in computer architecture, and formal methods, in particular model checking. Communication and writing skills, teamwork motivation and eager to learn.
In line with CEA's commitment to integrating people with disabilities, this job is open to all.
Localisation du poste
Site
Saclay
Localisation du poste
France, Ile-de-France, Essonne (91)
Ville
Palaiseau
Critères candidat
Langues
Anglais (Intermédiaire)
Diplôme préparé
Bac+5 - Diplôme École d'ingénieurs
Demandeur
Disponibilité du poste
01/03/2025
Je me crée un espace candidat
