SSAC : Simulation et Analyse Statique pour la Modélisation de Cache de Niveau 2 // SSAC: Simulation and Static Analysis for L2 Cache Modeling

Les mémoires caches sont des composants clefs pour la performance des systèmes multi-coeurs.
Cependant, modéliser leur comportement devient une tâche complexe quand on considère des caches partagés, comme les caches L2, car plusieurs programmes accèdent en parallèle à cette même ressource.
Le sujet de cette thèse porte sur comment bien combiner deux méthodes existantes de modélisation de mémoires cache.
1. Simulation : Pour aider le dévelopement de plus en plus rapide de nouvelles plateformes, le protypage de plateforme utilise la simulation logicielle (comme QEMU ou gem5). Cela permet de commencer le dévelopement des programmes avant même que le dévelopement de la plateforme matérielle soit terminée (par exemple, tester de nouvelles politiques de cohérence de cache avant leur dévelopement matériel). Des travaux précédents à TIMA ont montré que la simulation de cache de niveau 2 par un plugin QEMU est un problème complexe dans un contexte de plateforme multi-coeur, en particulier dû au fait que la synchronisation de tous les accès au cache impacte grandement la performance du simulateur.
2. Analyse statique : Plusieurs méthodes d'analyses statiques ont été proposées pour garantir des propriétes d'un programme exécuté sur une plateforme donnée. Des travaux précédents à Verimag ont étudié des méthodes de sur-approximation de contenu de cache L1 pour garantir une borne supérieure du temps d'exécution et, en particulier, affiner le nombre de succés ou d'échec d'accés à la mémoire cache.

Un bon modèle de mémoire cache devrait décrire précisément son comportement, mais devrait aussi abstraire suffisamment de détails pour rester utilisable en pratique (en particulier, pour le passage à l'échelle).
Dans ce projet de thèse, nous proposons d'étudier comment ces deux approches standards de modélisation peuvent être combinées pour concevoir de meilleures approches de modélisation.
En particulier, nous étudierons dans cette thèse deux directions complémentaires pour la simulation et l'analyse de mémoires cache multi-niveau dans les plateformes multi-cœur :
1. comment les dernières avancées de la simulation de cache peuvent être utilisées en analyse statique pour affiner le contenu des modèles abstraits ?
2. comment les dernières avancées en analyse statique peuvent aider à améliorer la précision des simulations ?
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Memory caches are crucial components for multi-core system performance.
However, modeling their behavior becomes a complex task when one considers shared caches, such as L2 caches, due to multiple programs accessing to this same resource.
In this thesis, we aim at combining two cache modeling approaches.
1. Simulation: To cope with the rapid development of new platforms, prototyping often relies on software simulators (such as QEMU or gem5). It allows to develop programs on still under-development platforms, or even to help designing those platforms (e.g., testing new cache coherence policies before hardware design). Previous work in TIMA have shown, in particular, that simulating shared L2 caches as a plugin of QEMU is a difficult problem, especially in a multi-core context, as synchronizing all caches accesses impact the performance of the simulator.
2. Static analysis: Several static analysis techniques have been proposed to provide guarantees of a program running on a specific platform. Previous work in Verimag have studied methods to over-approximate the content of the L1 cache, to bound the access times in system with L1 caches.

A good modeling of a cache should accurately capture its behavior, but should also abstract enough details to remain practical for use (in particular, for scalability). In this thesis project, we aim to explore how both modeling approaches can work together to improve scalability without sacrificing too much precision — on the micro-architectural details for the simulation part (e.g., cache hit/misses count), and on the program properties for the static analysis part (e.g., execution time estimation).
Particularly, we propose to study two complementary directions, to guide the future of multi-level cache design and analysis:
1. how can lessons learned by cache simulator developers be used to better analyze multi-level caches, in particular to refine the abstractions used in static analyses?
2. can the recent improvements in caches static analyses help improve the performance of cache simulators, more specially in a multi-core context?
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/10/2026

Concours allocations

Université Grenoble Alpes

217 MSTII - Mathématiques, Sciences et technologies de l'information, Informatique

bonne capacité de restitution et de rédaction (notamment en anglais) Bonne connaissance des méthodes formelles et de l'architecture des ordinateurs, une connaissance de la modélisation de matériel est un plus.
Good level in writing scientific articles and communication in english Good knowledge in formal methods and hardware architecture, a good knowledge in hardware modeling would be a plus