Accès direct au contenu

CMLA

Version anglaise

aide

Verificarlo : Un outil de vérification du logiciel de calcul

Le logiciel de vérification automatique Verificarlo est développé par Christophe Denis (ENS Cachan), Pablo de Oliveira Castro et Eric Petit  (université de Versailles-de-Saint en Yvelines).


Démocratiser l'évaluation de la précision numérique dans le processus de  Vérification et Validation (V&V) d'un logiciel de simulation.

Cette démocratisation nécessite d'une part de limiter au maximum les modifications à apporter au logiciel  et d'autre part de fournir une interprétation des résultats compréhensibles pour des non experts en arithmétique flottante. L'expertise du CMLA s'est appliquée sur l'amélioration de la performance et de la performance du logiciel de calcul.

Pourquoi contrôler la précision numérique des résultats ?


Les codes de simulation numériques sont utilisés pour fournir une solution approchée d'un problème physique. Un code de simulation numérique peut par exemple modéliser le climat ou contrôler la tenue d'une pièce mécanique.

La démarche usuelle consiste tout d'abord à modéliser un comportement physique par des équations mathématiques. Ces équations mathématiques ne peuvent pas être résolues telles quelles sur un ordinateur car elles ne possèdent pas, hormis parfois pour des cas tests simples, de solutions analytiques.

Une étape de discrétisation des équations mathématiques permet de construire un algorithme de calcul fournissant une solution approchée des équations mathématiques. Les méthodes de discrétisation les plus connues sont les méthodes des différences finis, des volumes finis et des éléments finis. Les étapes de modélisation mathématique du problème et de discrétisation du problème entraînent des approximations au niveau de la solution de calcul.

Pour accréditer les résultats de calcul d'un code de simulation, ces approximations sont gérées et contrôlées dans le cadre d'un processus de V&V (Verification & Validation). L'ensemble infini et continu de valeurs réelles est approché par ensemble fini et discret de valeurs représentables sur un ordinateur : les nombres flottants.

Depuis 1984, la norme IEEE-754 définit une représentation standardisée  des nombres flottants ainsi que des règles d'arrondi. Cette norme permet d'obtenir le meilleur compromis possible entre la précision et l'étendue des nombres. De plus, elle a permis d'accroître significativement la portabilité d'un code de calcul sur différents ordinateurs. Cependant, il existe des effets indésirables du calcul en arithmétique flottante. Il est en particulier nécessaire à chaque étape de calcul d'arrondir le résultat c'est-à-dire choisir le nombre flottant représentant le résultat.

Ainsi,  contrairement au calcul manipulant des nombres réels, le calcul en arithmétique flottante :
- ne permet pas de représenter exactement tous les nombres réels sur un ordinateur  (erreur de représentation), c'est par exemple le cas pour la valeur flottante correspondante à la valeur réelle 0.1 ;
- propage des erreurs d'arrondi dans un code de calcul ;
- cause une perte de propriétés arithmétiques, par exemple l'addition flottante n'est plus associative.

Un logiciel numérique peut donc produire des résultats différents, par exemple en changeant le nombre de processeurs utilisés, la plate-forme de calcul ou les options de compilation utilisées. Ce phénomène de non reproductibilité numérique devient de plus en plus marqué en raison de l'utilisation massive de puissance de calcul. La question récurrente des développeurs et des utilisateurs d'un logiciel est de savoir si la non reproductibilité numérique est le signe d'un bogue ou dans le code.

Le but du logiciel Verificarlo est d'apporter des éléments de réponse à cette question pour des non experts en arithmétique flottante et à moindre coût. Ce logiciel permet également de gérer au mieux le compromis entre la performance, la précision et la consommation énergétique de simulations  numériques.

Description rapide du logiciel


Verificarlo implémente automatiquement à la compilation l'arithmétique de Monte-Carlo (MCA) pour mener une analyse de sensibilité des résultats vis-à-vis de l'arithmétique flottante.  La figure suivante présente le principe général de Verificarlo :






Verificarlo permet de mener une analyse de sensibilité par rapport au options de compilation de LLVM.  Une prochaine version de Verificarlo contiendra un outil de post-traitement automatique pour faciliter l'analyse du développeur. Le logiciel Verificarlo a tout d'abord été testé sur des exemples académiques écrits en Fortran ou C. Les résultats ont été comparés avec un outil de débogage numérique qui nécessite de transformer le code source. Le lecteur pourra consulter [1] pour obtenir plus de précision sur le résultat de cette comparaison.

Exemple d'utilisation industrielle


Une collaboration est en cours entre le CMLA et EDF R&D pour mener à l'aide de Verificarlo une analyse de la précision numérique produit par le logiciel de modélisation en mécanique des structures Code_Aster (avec un support scientifique de l'UVSQ).

C'est un véritable défi pour Verificarlo puisque Code_Aster, d'une part contient plus d'un million de lignes de code source (écrit en langage C, C++, et Fortran) de code et d'autre part utilise des bibliothèques de calcul scientifique (MUMPS, LAPACK, BLAS, ..).

Les premiers résultats obtenus sont très encourageants. L'instrumentation de Code_Aster s'est effectuée automatiquement à la compilation sans modifier une seule ligne de son code source, ce qui valide la preuve de concept de Verificarlo. Ainsi, des premiers résultats  de l'analyse ont été partagés rapidement avec EDF R&D. 

Nul doute que d'autres travaux scientifiques devraient émerger grâce à ce logiciel dans ce secteur de la simulation numérique, aujourd'hui en plein essor.








Sponsors


















Pour aller plus loin...

Le projet Verificarlo est à la recherche d'applications pour que cet outil soit proche des besoins des logiciels.

N'hésitez pas à nous contacter si vous souhaitez tester Verificarlo, lancer une collaboration ou échanger.

Références

[1] Christophe Denis, Pablo de Oliveira Castro, Eric Petit, "Verificarlo: checking floating point accuracy through Monte Carlo Arithmetic", 23rd IEEE International  Symposium on Computer Arithmetic (ARITH'23), 2016.

[2] Christophe Denis, "Checking the floating point accuracy of Scientific Codes  through Monte Carlo Arithmetic", SIAM Conference on Parallel Processing (SIAM PP 16), Paris, 2016.