Thèse Ssac Simulation et Analyse Statique pour la Modélisation de Cache de Niveau 2 H/F - Doctorat.Gouv.Fr

Établissement : Université Grenoble Alpes École doctorale : MSTII - Mathématiques, Sciences et technologies de l'information, Informatique Laboratoire de recherche : VERIMAG Direction de la thèse : Claire MAIZA ORCID 0000000259776685 Début de la thèse : 2026-10-01 Date limite de candidature : 2026-06-22T23:59:59 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-coeur :
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 ? Ce projet de thèse est à la frontière entre deux domaines d'expertise : l'analyse statique de programmes, et la simulation de micro-architecture.
Ces deux domaines sont à l'interface entre logiciel et matériel, l'équipe d'encadrement étant composée d'expert(e)s habitué(e)s à travailler à cette interface.
En particulier, cette équipe propose une expertise complémentaire entre modélisation, implémentation et simulation des architectures modernes.
Les laboratoires Verimag et TIMA sont reconnus à l'international pour leurs expertises respectives dans ces domaines, et nous pensons que le ou la candidat(e) profitera grandement de ce contexte. Améliorations des techniques de modélisation existantes pour les caches L2 dans les systèmes multi-coeur, que ce soit pour l'analyse statique (notamment, pour la sûreté des systèmes) ou pour la simulation (en particulier, pour le prototypage des architectures de demain). familiarisation avec les méthodes existantes de modélisation, étude des avantages et inconvénients des deux familles considérées (simulation et analyse statique), et proposition d'améliorations des logiciels/méthodes existantes, avec validation empirique sur des bancs de programmes à l'état de l'art

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.

• Amélioration continue