Formal Investigation Of Timing Anomalies And Memory Interference In Multicore Wcet Analysis H/F CEA

Critical systems, such as those found in the automotive and avionics domains, are subject to stringent requirements, including the guarantee that mandatory deadlines are never missed. Consequently, the design, implementation, and analysis of these systems are governed by strict regulations, formalized in industry standards that specify such requirements. When deadlines are concerned, the key aspect is timing. To ensure deadline compliance, the timing validation of critical systems is typically performed through a specialized analysis known as Worst-Case Execution Time (WCET) analysis [1]. In essence, WCET analysis aims to provide safe and precise upper bounds on the execution time of a program running on a specific architecture. As a result, it inherently relies on a joint consideration of hardware and software aspects.
In a general setting, this hardware-software consideration involves, on the hardware side, a multicore architecture, and on the software side, a multi-threaded application or any software representation consisting of well-identifiable computation tasks. In this context, two issues threaten the computation of safe and precise WCET bounds: timing anomalies (TAs) and memory interferences (MI). Timing anomalies [2] are counter-intuitive behaviors in which a locally worst-case execution does not lead to a globally worst-case execution time. Memory interferences [3] arise when multiple application threads or tasks concurrently access shared resources, such as memory components, inducing additional delays that must be safely bounded through a dedicated analysis. In this internship, we focus on shared resources as the primary source of complexity in developing a WCET analysis and aim to investigate its interaction between TAs on the one hand and processor design and MI on the other hand. This investigation may, for instance, be carried out using formal modeling and verification frameworks such as Romeo [4] or F* [5], which enables exhaustive exploration of joint hardware-software models. The objective is to formally establish provable timing behavior properties of the analyzed critical systems, accounting for both TAs and MI.
The internship may pursue one of the following objectives:
- the practical characterization of the relationship between timing anomalies and memory interferences on a formal joint hardware-software model;
- the design and implementation of a WCET analysis that exploits such a characterization while maintaining safety guarantees.
[1] R. Wilhelm et al. The worst-case execution-time problem - overview of methods and survey of tools, in TECS 2008
[2] B. Binder et al. The role of causality in a formal definition of timing anomalies, in RTCSA 2022
[3] C. Maiza et al. A survey of timing verification techniques for multi-core real-time systems, in ACM Comput. Surv 2019
[4] D. Lime et al. Romeo - a parametric model-checker for Petri nets with stopwatches, in TACAS 2009
[5] www.fstar-lang.org

#CEA-List