Thèse Transformations Source à Source Prouvées pour l'Architecture Arm H/F - Doctorat.Gouv.Fr

Établissement : Mines Paris-PSL École doctorale : ISMME - Ingénierie des Systèmes, Matériaux, Mécanique, Énergétique Laboratoire de recherche : Mathématiques et Systèmes Direction de la thèse : Olivier HERMANT ORCID 0000000162331903 Début de la thèse : 2026-10-01 Date limite de candidature : 2026-10-31T23:59:59 Ce projet de thèse s'inscrit dans le cadre de la compilation source-à-source des programmes, qui permet des optimisations de haut niveau, portables sur différentes architectures. Il cible des programmes et des librairies, développées pour architecture x86, que le partenaire industriel de cette thèse, ARM, souhaite migrer vers son architecture de manière efficace et sûre. Il s'agira notamment de prendre en compte les instructions vectorielles et d'exploiter les fonctions intrinsèques, ainsi que d'utiliser des outils permettant de garantir formellement que les traductions préservent le comportement sémantique du code. L'optimisation source-à-source consiste à transformer automatiquement un code existant en un code fonctionnellement équivalent mais plus efficace, tout en restant au même niveau d'abstraction. Cette approche offre de nombreux avantages : elle garantit la portabilité sur différentes plateformes matérielles et permet une exploitation optimale des spécificités de chaque architecture, sans compromettre la lisibilité ni la maintenabilité du code. Contrairement aux optimisations de bas niveau, souvent limitées à un seul compilateur ou à une seule architecture, les transformations source-à-source sont plus générales et scalables, ce qui facilite leur intégration dans des chaînes de compilation hétérogènes. Elles constituent ainsi un levier essentiel pour un développement logiciel durable et efficace sur des systèmes de plus en plus diversifiés. L'objectif de la thèse est de proposer des méthodes d'aide à la migration / optimisation de code adaptées aux contraintes industrielles sur des bases de code réelles et s'intégrant aux flots de développement moderne. Plus spécifiquement, la thèse visera à l'optimisation des performances de noyaux de calculs critiques et de calculs IA sur les machines modernes à base de processeurs Arm, avec un focus sur la portabilité au sein des architectures Arm et l'exploitation efficace de la vectorisation et du parallélisme, ainsi que l'intégration réaliste dans des chaînes de développement.
La thèse inclura le développement d'un démonstrateur évolutif et intelligent combinant :
- l'exploration structurée de scenarios de transformation,
- d'optimisation en performance,
- d'aide à la décision avec de l'IA,
- tout en fournissant des garanties de correction formelles.

Compilation
Optimisation
Langages de programmation
Méthodes formelles
Langage C