Production de code haute performance digne de confiance à travers des transformations source-à-source – OptiTrust

Transformer une implémentation naïve d'un algorithme en un code haute performance peut prendre des des mois de travail d'un programmeur expert. En effet, il faut arriver à tirer parti des instructions vectorielles, des différents cœurs, et des différents serveurs, ainsi qu'à optimiser la représentation des données en mémoire, maximiser la localité des opérations, et à éviter la saturation de la bande passante. En général, faute de pouvoir se contenter de quelques annotations ou de pouvoir utiliser un langage spécifique, le programmeur est contraint d'écrire à la main du code combinant des dizaines d'optimisations. Cette approche est non seulement longue et fastidieuse, mais elle dégrade la lisibilité du code, rend délicat sa maintenance, et risque d'introduire des bugs. L'outil alpha-OptiTrust permet de dériver un code HPC à travers une série de transformations source-à-source, pilotées interactivement par le programmeur. Cette approche a fait ses preuves dans des domaines niches, comme le traitement d'image ou le "machine learning". Alpha-OptiTrust la généralise a du code arbitraire. Le présent projet vise à obtenir des garanties formelles sur la correction des codes produits. Pour cela, nous vérifierons à travers des preuves mécanisées l'implémentation des transformations. Comme certaines de ces transformations ne sont correctes que sous des hypothèses spécifiques, nous formaliserons ces hypothèses et nous étudierons lesquelles peuvent être validées par des analyses statiques. Pour traiter les hypothèses plus complexes, nous étendrons OptiTrust pour transformer non seulement du code mais également des invariants formels attachés au code. Cela permettra d'exploiter des invariants exprimés sur le code d'origine, pour justifier les hypothèses des transformations appliquées à la n-ième étape. Nous appliquerons OptiTrust à plusieurs étude de cas, notamment des simulations numériques en physique des fluides et en physique des plasmas.