Thèse Vérification des Noyaux Gpu dans le Contexte de la Programmation à Base de Tâches Application à Starpu - Kokkos H/F - Doctorat.Gouv.Fr

Établissement : Université de Bordeaux École doctorale : Mathématiques et Informatique Laboratoire de recherche : LaBRI - Laboratoire Bordelais de Recherche en Informatique Direction de la thèse : Samuel THIBAULT ORCID 000000016411809X Début de la thèse : 2026-11-01 Date limite de candidature : 2026-09-30T23:59:59 L'utilisation croissante des accélérateurs de calcul GPU se confirme à travers le classement TOP500, qui recense les supercalculateurs les plus puissants au monde. Dans ce contexte, écrire des programmes corrects et efficaces pour les GPU constitue un enjeu critique. La programmation parallèle est connue pour être particulièrement difficile, avec des symptômes complexes à identifier tels que des résultats non déterministes ou des corruptions de données silencieuses. Dans le cas de la programmation pour GPU, cette difficulté est très largement amplifiée, les débordements de tampons étant très largement non capturés par l'environnement d'exécution. Les potentielles pertes de performance sont également démultipliées par l'architecture particulière de ces plateformes. Ces obstacles sont ainsi extrêmement complexes à identifier à grande échelle.


Les méthodes actuelles de vérification des noyaux GPU se divisent principalement en deux approches: les approches statiques et les approches dynamiques. Les approches statiques [NGB26,
CKPT25, CLLZ23, LLS+12] sont capables de détecter les erreurs quelque soit le jeu d'entrée mais sont basées sur de la vérification formelle et souffrent souvent d'un sur-coût d'analyse majeur, de faux positifs, ou nécessitent des annotations manuelles lourdes de la part du développeur ou de la développeuse.
Les approches dynamiques s [OLG25, JBG24, EPP+17, AGR+18, PGD18, KGB20, WOZ+20, KB21] sont précises mais sur le jeu de données utilisé et ne garantissent pas l'absence totale d'erreur. Elles augmentent également le temps d'exécution. Une approche récente [CZD+26] utilise des LLMs pour générer automatiquement des annotations destinées à un outil de vérification formelle basé sur un solveur SMT, afin de prouver l'absence d'accès concurrent dans les noyaux CUDA. Cette approche souffre des mêmes inconvénients que les approches statiques.

De plus, une grande partie de l'état de l'art se focalise quasi exclusivement sur la détection des accès mémoire concurrents. Si ces erreurs sont majeures, d'autres anomalies sont négligées: synchronisations de intra-wraps, incohérences de dimensions de matrices, accès incorrects à des données.

Une des raisons pour les limitations des approches actuelles est un manque d'information sur les données manipulées, et notamment leurs tailles et leurs formes, à moins d'imposer l'ajout de lourdes annotations de code. Le code hôte de soumission de kernels pourrait fournir cette information, mais la plupart des outils existant ne l'exploite pas, en partie car elle reste difficile à l'y obtenir.

Par ailleurs, sur la décennie passée, la programmation à base de tâches est progressivement devenu un paradigme de plus en plus utilisé par les codes HPC, dans des classes d'applications diverses. Dans ce cadre, l'expression des tailles et formes des données fait partie du modèle de programmation en lui-même. Ainsi, lors de l'exécution d'une tâche, ces informations sont disponibles de manière fiable au moment de la soumission d'un kernel au GPU. Il devient alors possible de vérifier les paramètres de cette soumission, et d'apporter cette information à la vérification du code du kernel, qui n'a plus besoin de reposer sur des heuristiques imprécises. La thèse se déroulera en collaboration avec le CEA Cette thèse a pour objectif de concevoir une approche d'analyse statique/dynamique exacte, transparente pour l'utilisateur (sans annotation de code) et intégrée au compilateur, capable de vérifier la correction globale d'un noyau GPU et de déceler les opportunités d'optimisation de ces noyaux, exécutés au sein d'un modèle de programmation à base de tâches.

Le modèle de programmation à base de tâches impose au développeur de déclarer explicitement les dépendances et les accès mémoire (données d'entrée/sortie, tailles et pointeurs manipulés). Ces méta-données constituent un point d'appui privilégié pour mener une analyse statique précise. En étudiant le code hôte, nous avons donc la possibilité de récupérer des informations pour aider à:

- détecter les accès incorrects à des données utilisées sur GPU.
- détecter des patterns d'accès concurrents avec race conditions
- vérifier les synchro de wraps etc.
- et autres règles de calcul GPU

- Solides bases en programmation C et en programmation parallèle (threads, OpenMP, GPU ou équivalent)
- Environnement de développement C de type Unix
- Goût pour l'expérimentation : conception de protocoles de mesure, analyse critique des performances obtenues.
- Autonomie, rigueur et curiosité scientifique ; aptitude à mener un travail de recherche sur trois ans.
- Maîtrise de l'anglais scientifique, à l'écrit comme à l'oral.