Dans un compilateur (par exemple pour le langage C), il y a plusieurs phases qui relèvent de la résolution de problèmes d’optimisation combinatoire : l’ordonnancement des instructions, le placement des opérandes dans les registres. Ces problèmes sont habituellement résolus par des heuristiques.
CompCert est un compilateur formellement vérifié, c’est-à-dire qu’il y a des preuves mathématiques dont chaque étape a été vérifiée en machine (par l’assistant de preuve Coq). Il n’est cependant pas nécessaire de vérifier que chaque algorithme est correct : on peut lancer un algorithme auquel on ne fait pas confiance, et vérifier son résultat à l’aide d’une procédure formellement prouvée (si cette procédure détecte un problème, la compilation échoue mais au moins on ne produit pas de code incorrect).
La branche "chamois" de CompCert dispose d’ordonnancements d’instructions, mais ceux-ci sont perfectibles.
Le sujet du stage est la mise en œuvre de meilleurs algorithmes d’ordonnancement et/ou d’allocation de registres, soit heuristiques soit par réduction vers des problèmes d’optimisation combinatoire confiés à des solveurs externes.
contacts : David Monniaux et Sylvain Boulmé
