Description
Date depot: 1 janvier 1900
Titre: Vérification numérique de logiciels de calcul industriels
Directrice de thèse:
Fabienne JEZEQUEL (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Le projet décrit ci-après s'inscrit dans le cadre d'une thèse CIFRE
qui sera effectuée à EDF R&D et au LIP6.
Pour exploiter au mieux leurs moyens de production, les industriels
comme EDF utilisent de manière croissante des Outils de Calcul
Scientifique (nommés OCS dans la suite de ce projet). La
vérification, la validation et l'estimation des incertitudes dans les
OCS sont devenues indispensables en particulier dans le cadre de la
démonstration de sûreté nucléaire.
Les travaux de thèse menés par S. Montan [2] ont montré la
pertinence de l'utilisation, dans un contexte industriel, de la
bibliothèque CADNA (http://www.lip6.fr/cadna) [1] développée au LIP6.
CADNA implémente la méthode CESTAC [3] qui permet d'estimer la
propagation d'erreurs d'arrondi grâce à trois exécutions du programme
effectuées avec un mode d'arrondi aléatoire. Les travaux de S. Montan
ont permis de localiser et de corriger un nombre important
d'instabilités dans le code Telemac2D développé à EDF, conduisant à
une amélioration de la reproductibilité numérique (les résultats
devenant moins sensibles au nombre de processeurs).
Cette thèse a cependant soulevé deux problèmes dans la gestion des
bibliothèques externes :
-# CADNA nécessite d'instrumenter le code source et celui des bibliothèques externes qu'il utilise. Selon les codes, cela peut être fastidieux et même impossible dans le cas où on ne dispose pas des sources.
-# Une fois les problèmes d'erreurs d'arrondi détectés, une des méthodes de correction est l'utilisation d'algorithmes compensés. Ces algorithmes, satisfaisants en arrondi au plus près, doivent être étudiés avec le mode d'arrondi aléatoire. Le but est de pouvoir analyser avec CADNA les résultats produits par un OCS utilisant des algorithmes compensés.
Le code source des OCS peut être découpé en composants appartenant à
plusieurs catégories :
a) des algorithmes dont on ne connaît pas la qualité numérique, parmi lesquels on peut distinguer :
1. les codes développés en interne à EDF, potentiellement instrumentables ;
2. des bibliothèques externes, dont le code source n'est pas disponible ou instrumentable ;
b) des algorithmes pour lesquels une information sur la qualité
numérique des résultats est connue a priori. On peut citer à
titre d'exemple : les algorithmes de sommation compensée, dont la
précision est garantie par des résultats théoriques, certains appels
de bibliothèque standard (cos, sin, log, ...) pour lesquels
l'implémentation garantit un résultat à la précision machine.
Ce sujet de thèse vise des avancées sur les deux aspects limitants de
la gestion des bibliothèques avec la méthode CESTAC identifiés lors de la thèse de S. Montan. On souhaite conserver la possibilité offerte par CADNA de localiser les instabilités dans les composants de type
(a1) des OCS, tout en profitant de l'extrême facilité d'utilisation
des approches par instrumentation binaire sur les composants (a2). De
plus, on souhaite être en mesure de tirer parti des informations
connues a priori sur les bibliothèques de type (b) pour effectuer, de
manière efficace, une estimation plus fine de l'erreur commise. Enfin
l'optimisation de la précision dans un code constitue un objectif à
long terme de cette thèse.
Références :
[1] F. Jézéquel and J-M. Chesneaux. CADNA : a library for estimating
round-off error propagation. Computer Physics Communications,
178(12) :933– 955, 2008.
[2] S. Montan. Sur la validation numérique des codes de calcul industriels.
Thèse de doctorat, LIP6, UPMC, 2013.
[3] J. Vignes. A stochastic arithmetic for reliable scientific
computation. Math. Comput. Simulation, 35 :233–261, 1993.
Doctorant.e: Picot Romain