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).

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.