Pause
Lecture
Moteur de recherche d'offres d'emploi CEA

Benchmarking the scalability of model-checker-based detection of timing anomalies H/F


Vacancy details

General information

Organisation

The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, development and innovation in four main areas :
• defence and security,
• nuclear energy (fission and fusion),
• technological research for industry,
• fundamental research in the physical sciences and life sciences.

Drawing on its widely acknowledged expertise, and thanks to its 16000 technicians, engineers, researchers and staff, the CEA actively participates in collaborative projects with a large number of academic and industrial partners.

The CEA is established in ten centers spread throughout France
  

Reference

2023-30049  

Description de l'unité

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.

Position description

Category

Mathematics, information, scientific, software

Contract

Internship

Job title

Benchmarking the scalability of model-checker-based detection of timing anomalies H/F

Subject

Systems with critical safety requirements, such as autonomous vehicles and modern avionic computers, must adhere to stringent timing constraints. Failure to meet these constraints, such as missing a deadline, can lead to serious malfunctions. Consequently, it is crucial to calculate reliable timing bounds for these systems. Worst-Case Execution Time (WCET) analyses [1] aim to determine accurate and preferably tight worst-case execution bounds. These analyses use convenient abstractions to explore all possible execution paths of a program running on a computer architecture.


The presence of Timing Anomalies (TA) [2] complicates this process. TAs are characterized by counterintuitive behavior where the local worst-case timing, often caused by a cache miss, does not necessarily translate into the global worst-case performance. Consequently, addressing TAs requires an exhaustive exploration of the reachable hardware states, a task that is costly or even prohibitive.

Contract duration (months)

6

Job description


The LECA laboratory has developed a framewok [3, 4] to identify Timing Anomalies (TAs) within programs. This framework is built upon a formal model of a representative Out-of-Order (OoO) processor pipeline described using the TLA+ high-level language [5]. Program specifications are generated from input C source codes using the output of the gem5 simulator [6]. Local timing variations are introduced through heuristics targeting the latencies of memory instructions. Subsequently, TAs are expressed as hyper-properties in TLA+ and formally verified using the TLC model-checker over a combined formal model of the pipeline and a program. This model-checker-based workflow has proven successful in detecting TAs using the TACLe benchmarks [7], but for a limited number of instructions and memory access variations.

 

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. This involves to incorporate the notion of basic blocks, the atomic analysis unit in static WCET analyses, into the formal program specification. This enhancement will enable to study whether TAs can propagate across multiple basic blocks and help to capture the limitations 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. This may involve utilizing the output of WCET cache analyses to narrow down the set of latency variations, adjusting the verification instant for TA detection, or exploring the use of different model-checkers, such as the Apalache symbolic model-checker for TLA+ [8].

 

[1] Reinhard Wilhelm et al. The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst., 7(3):36:1–36:53, 2008.
[2] T. Lundqvist and P. Stenström, “Timing anomalies in dynamically scheduled microprocessors,” in Real-Time Systems Symposium, 1999.
[3] Mihail Asavoae, Belgacem Ben Hedia, Mathieu Jan. 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).
[4] B. Binder et al. "Is This Still Normal? Putting Definitions of Timing Anomalies to the Test," RTCSA 2021, Houston, TX, USA, pp. 139-148.
[5] Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc. (2002)
[6] Jason Lowe-Power et al. The gem5 Simulator: Version 20.0+. CoRR abs/2007.03152
[7] Heiko Falk et al. “TACLeBench: A Benchmark Collection to Support Worst-Case Execution Time Research”. WCET 2016
[8] Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. 2019. TLA+ model checking made symbolic. Proc. ACM Program. Lang. 3, OOPSLA, Article 123 (October 2019).

Methods / Means

TLA+, TLC, gem5

Applicant Profile

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.

Position location

Site

Saclay

Job location

France, Ile-de-France, Essonne (91)

Location

  Palaiseau

Requester

Position start date

01/03/2024