Description

Le développement logiciel occupe une place particulière et souvent essentielle au sein des organismes de recherche : valorisation des résultats, diffusion de la connaissance, vecteur d'échanges et de collaborations, ... sans oublier que leur utilisation peut être au cœur de la publication scientifique.

Alors que la recherche de performance fait l'objet de vifs intérêts (souvent justifiés) au sein du processus de développement et que les formations dans ce domaine sont assez nombreuses, il semble que certaines questions, pourtant essentielles, sont souvent négligées. Les méthodes numériques employées pour résoudre un problème sont souvent maîtrisées au sens où l'on connaît les erreurs de méthode (ordre d'un schéma numérique, erreur réalisée sur la résolution d'un système linéaire, ...). Il n'en est pas de même pour les erreurs d'arrondi faites lors de la résolution numérique. Les différentes opérations en arithmétiques flottantes qu'effectuent ces algorithmes de résolution peuvent aboutir à des résultats différents selon l'architecture, le compilateur, le système d'exploitation, le sens des opérations, ...

Se posent alors des questions essentielles qui ne sont pas forcément traitées par les développeurs de logiciels : Quel crédit numérique peut-on accorder à un logiciel ? Quelle est la précision des résultats obtenus ? Ces résultats sont-ils reproductibles (dans le temps et dans d'autres configurations) ?

  • Précision

La précision des calculs effectués par un logiciel scientifique doit être, au minimum mesurée, sinon maîtrisée. Car, même sans parler de bug (au sens erreur de programmation), tout logiciel scientifique manipulant des réels (ou plus exactement un sous ensemble de ℝ) est amené à réaliser des arrondis, des approximations qui, s'ils ne sont pas mesurés et contenus, peuvent mettre à mal le crédit que l'on est en droit de lui accorder.

  • Reproductibilité

Le crédit d'un logiciel scientifique et des publications s'appuyant sur ses résultats passe aussi par un travail portant sur la « reproductibilité » du logiciel : il faut pouvoir s'assurer que les résultats obtenus à un instant donné dans une configuration donnée puissent être « reproduits » dans le temps et dans des contextes informatiques différents (compilateur, architecture, système d'exploitation, ...) ou, au moins, être capable de mesurer et justifier ces différences.

Programme

lundi 25/03

14:00 15:30 Télécharger le support

De calculer juste à calculer au plus juste

Florent de Dinechin (École Normale Supérieure de Lyon)

L'objectif de cette école est la maîtrise de la précision et de la reproductibilité en calcul numérique. La communauté française est très active sur tous les fronts de cette problématique, et cette école va donner un bon panorama des outils qu'elle développe. Cette introduction tentera de montrer que l'impact de ces travaux est amené à déborder largement du calcul numérique classique : la maîtrise de la précision pourrait jouer un rôle important, dans les années qui viennent, dans l'éternelle course à la performance.

La double-précision, généralisée et normalisée depuis les années 80, nous gâte avec 16 chiffres décimaux significatifs. Mais quelle application a besoin d'une telle précision ? On ne se posait pas vraiment la question tant que la loi de Moore nous offrait cette gabegie de précision avec une performance croissante. Mais en 2004, la loi de Moore s'est heurté au "mur de la fréquence" : la fréquence a cessé d'augmenter. Pour continuer à offrir plus de performance, l'industrie s'est tourné vers le parallélisme (SIMD et multicoeur), et la capacité de calcul flottant a continué d'augmenter -- la reproductibilité en moins. Mais il est prévu que cette approche se heurte à un nouveau mur, celui de la dissipation d'énergie, d'ici 5 à 10 ans.

Et voilà pourquoi on voit désormais dans les conférences des exposés d'Intel ou de Microsoft réclamant des outils logiciels qui permettraient de ne pas calculer plus précis que ce que l'application nécessite. Non pour la beauté de la chose, mais dans le but de calculer toujours plus, et désormais pour le même prix.

Mais pour calculer au plus juste, il faut comprendre ce qu'on calcule, et il faut comprendre de quelle précision l'application a besoin. Bienvenue à l'école Précision et Reproductiblité du Calcul Numérique !

15:30 16:00 Pas de support disponible Pas de résumé disponible

Pause

16:00 19:00 Télécharger le support

Arithmétique flottante

Jean-Michel Muller (École Normale Supérieure de Lyon)

Je ferai tout d'abord une présentation générale de l'arithmétique virgule flottante (définitions, propriétés élémentaires, écueils divers). Par la suite, je présenterai quelques détails du standard IEEE 754-2008, en insistant sur la notion d'arrondi correct, qui est centrale lorsqu'on a comme but la reproductibilité des calculs, et qui permet de construire des algorithmes très utiles et de prouver leur comportement. Je terminerai en présentant de tels algorithmes.

mardi 26/03

09:00 10:30 Télécharger le support

Arithmétique flottante en précision arbitraire

Vincent Lefèvre (INRIA Grenoble - Rhône-Alpes / LIP, ENS-Lyon)

Je présenterai MPFR, une bibliothèque de calcul à virgule flottante en précision arbitraire. Une des particularités est une spécification complète de l'arithmétique (modes d'arrondi, arrondi correct, exceptions...) s'inspirant des bonnes idées de la norme IEEE 754 et permettant notamment la reproductibilité des résultats sur les différentes plateformes et avec les différentes versions de MPFR, tout en étant efficace. Je détaillerai aussi la façon dont MPFR est testée et donnerai quelques exemples simples. La session se composera d'une heure de présentation et de 2 heures de TP.
10:30 11:00 Pas de support disponible Pas de résumé disponible

Pause

11:00 12:30 Pas de support disponible

Arithmétique flottante en précision arbitraire (suite)

Vincent Lefèvre (INRIA Grenoble - Rhône-Alpes / LIP, ENS-Lyon)

Suite
12:30 14:00 Pas de support disponible Pas de résumé disponible

Repas

14:00 15:30

Arithmétique stochastique

Fabienne Jézéquel et Jean-Luc Lamotte (LIP6)

Télécharger le support Cours
Télécharger le support TPs
Télécharger le support Exercices
L'Arithmétique Stochastique Discrète (ASD) est une méthode automatique d'analyse d'erreur d'arrondi fondée sur une approche probabiliste. L'ASD consiste à exécuter un programme plusieurs fois de manière synchrone en utilisant un mode d'arrondi aléatoire, ce qui permet d'estimer le nombre de chiffres significatifs exacts des résultats. La bibliothèque CADNA, qui implémente l'ASD, permet dans un code scientifique en C ou en Fortran d'estimer la qualité numérique des résultats et de détecter les instabilités numériques générées pendant l'exécution. En outre, CADNA permet de développer de nouvelles méthodologies de programmation et ainsi d'optimiser les critères de convergence des algorithmes itératifs. Lors de cette école thématique, nous présenterons les principes de l'ASD et de la bibliothèque CADNA. Les TP permettront aux participants de se confronter au débogage numérique et à l'étude de la stabilité numérique via quelques exemples.
15:30 16:00 Pas de support disponible Pas de résumé disponible

Pause

16:00 17:30 Pas de support disponible

Arithmétique stochastique (suite)

Fabienne Jézéquel et Jean-Luc Lamotte (LIP6)

Suite

mercredi 27/03

09:00 10:30

Conception d'un algorithme numérique correct

Christoph Lauter (Équipe PEQUAN - LIP6 - UPMC Paris 6) et Guillaume Melquiond (Inria Saclay--Île-de-France & LRI, CNRS UMR 8623, Université Paris-Sud)

Télécharger le support Cours et TP
Télécharger le support Code
Une confiance élevée dans les codes en virgule flottante exige la preuve de propriétés numériques sur les valeurs intermédiaires et finales. Il s'agit par exemple de garantir que la valeur d'une variable reste dans un certain intervalle, ou bien que son erreur relative par rapport à une valeur idéale reste bornée. Ces propriétés peuvent exiger un lourd travail de preuve qui peut être réduit à néant par le moindre changement apporté au code, par exemple à des fins de maintenance ou d'optimisation. Concevoir et vérifier un programme en virgule flottante à la main est donc un processus fastidieux et entaché de nombreuses erreurs. Ce cours mettra l'accent sur des méthodes et outils qui offrent un environnement sûr pour le développement de code numérique. Une partie du cours sera consacrée à la production d'approximations polynomiales précises de fonctions mathématiques à l'aide l'outil Sollya. L'autre partie sera consacrée à la vérification formelle de propriétés sur les erreurs d'arrondi à l'aide de l'outil de Gappa. L'exemple de l'implantation en virgule flottante d'une fonction mathématique servira de fil conducteur à ce cours.
10:30 11:00 Pas de support disponible Pas de résumé disponible

Pause

11:00 12:30 Pas de support disponible

Conception d'un algorithme numérique correct (suite)

Christoph Lauter (Équipe PEQUAN - LIP6 - UPMC Paris 6) et Guillaume Melquiond (Inria Saclay--Île-de-France & LRI, CNRS UMR 8623, Université Paris-Sud)

Suite
12:30 14:00 Pas de support disponible Pas de résumé disponible

Repas

14:00 15:30 Pas de support disponible

Conception d'un algorithme numérique correct (suite)

Christoph Lauter (Équipe PEQUAN - LIP6 - UPMC Paris 6) et Guillaume Melquiond (Inria Saclay--Île-de-France & LRI, CNRS UMR 8623, Université Paris-Sud)

Suite
15:30 16:00 Pas de support disponible Pas de résumé disponible

Pause

16:00 17:30 Pas de support disponible

Conception d'un algorithme numérique correct (suite)

Christoph Lauter (Équipe PEQUAN - LIP6 - UPMC Paris 6) et Guillaume Melquiond (Inria Saclay--Île-de-France & LRI, CNRS UMR 8623, Université Paris-Sud)

Suite

jeudi 28/03

09:00 10:30

Arithmétique flottante par intervalles

Nathalie Revol (Inria, ENS de Lyon, LIP) et Philippe Théveny (ENS de Lyon, LIP)

Télécharger le support Cours et TP
Télécharger le support Exercices

Ce cours sera suivi d'un TP qui permettra de mettre en œuvre l'arithmétique par intervalles, mais surtout d'illustrer les différents phénomènes présentés en cours. Dans ce cours, nous commencerons par définir l'arithmétique par intervalles : objets et opérations arithmétiques. Cette arithmétique permet de calculer avec des ensembles plutôt que des nombres. Si les entrées sont des encadrements de valeurs exactes (non exactement représentables, comme π, ou valeurs mesurées à une erreur de mesure près), les résultats des calculs sont des encadrements des résultats exacts. Cette arithmétique donne donc des résultats garantis; cependant une utilisation avertie permet de réellement en tirer parti, comme nous le montrerons sur quelques exemples. Nous survolerons quelques "variantes" qui permettent de réduire la largeur des résultats, autrement dit d'améliorer la précision atteinte. Enfin, la question de la (non-)reproductibilité des calculs sera abordée à travers une brève présentation des difficultés rencontrées lorsque l'on vise à obtenir une implantation efficace en pratique.

Pour le TP, on utilisera la bibliothèque C d'arithmétique par intervalles en précision arbitraire MPFI.

10:30 11:00 Pas de support disponible Pas de résumé disponible

Pause

11:00 12:30 Pas de support disponible

Arithmétique flottante par intervalles

Nathalie Revol (INRIA, ENS de Lyon, LIP) et Philippe Théveny (ENS de Lyon, LIP)

Suite
12:30 14:00 Pas de support disponible Pas de résumé disponible

Repas

14:00 15:30 Télécharger le support

La reproductibilité dans la recherche assistée par ordinateur

Konrad Hinsen (Centre de Biophysique Moléculaire, CNRS)

La reproductibilité est en train de devenir un critère pour évaluer la qualité de résultats de recherche obtenus par le calcul. Si un autre chercheur peut reproduire les résultats publiés dans un article, ceux-ci sont plus crédibles, car un bon nombre d'erreurs et de tricheries peuvent être considérées peu probables. Mais en pratique, la reproductibilité n'est pas facile à atteindre: il faut conserver une trace détaillé des logiciels ainsi que des entrées et sorties, et il faut publier l'ensemble de ces informations dans une forme compréhensible et utilisable par d'autres chercheurs. Nous présenterons les différents aspects de la reproductibilité ainsi que des outils qui aident à y arriver.

Rencontre de Réflexion autour de la Recherche Reproductible (R4) : http://cascimodot.fdpoisson.fr/?q=node/51

Inscription à la liste de diffusion "recherche reproductible" : http://listes.univ-orleans.fr/sympa/subscribe/recherche-reproductible

15:30 16:00 Pas de support disponible Pas de résumé disponible

Pause

16:00 17:30 Télécharger le support

Lepton

Sébastien Li-Thiao-Té (LAGA, Paris 13)

Le logiciel Lepton est un outil pour la recherche computationnelle : implémentations d'algorithmes, écriture de rapports contenant le résultat de simulations numériques ou d'analyses de données, etc. Son objectif est faciliter la documentation des programmes, d'améliorer leur structure, et dans une certaine mesure d'annoter automatiquement les résultats des simulations.

Ce travail s'inscrit dans le domaine de la recherche reproductible. La question posée étant : comment faire pour que un travail de recherche publié soit réutilisable par d'autres collaborateurs et chercheurs, maintenant et dans le long terme.

vendredi 29/03

09:00 10:30 Télécharger le support

Sumatra

Konrad Hinsen (Centre de Biophysique Moléculaire, CNRS) et Andrew Davison (UNIC, CNRS)

Sumatra est un outil qui assure la traçabilité des résultats de calcul. Pour chaque calcul, Sumatra note les paramètres d'entrée, les versions du logiciel et de ses bibliothèques, et les fichiers générés. Avec ces informations, on peut refaire un calcul à l'identique, mais aussi s'assurer que les paramètres d'entrée qui ont mené à un résultat donné sont bien ce qu'on pense.
10:30 11:00 Pas de support disponible Pas de résumé disponible

Pause

11:00 12:30 Pas de support disponible

La reproductibilité dans la pratique aujourd'hui

Konrad Hinsen (Centre de Biophysique Moléculaire, CNRS)

Présentation d'un projet d'enquête et débat.
12:30 14:00 Pas de support disponible Pas de résumé disponible

Repas

Organisation

  • Stéphane Cordier (Laboratoire MAPMO, Orléans)
  • Loïc Gouarin (Laboratoire de Mathématiques d'Orsay)
  • Konrad Hinsen (CBM, Orléans)
  • Florent Langrognet (Laboratoire de Mathématiques de Besançon)

Comité Scientifique

  • Fabienne Jezequel (LIP6, Paris)
  • Jean-Luc Lamotte (LIP6, Paris)
  • Vincent Lefèvre (LIP, Lyon)
  • Nicolas Louvet (LIP, Lyon)
  • Christophe Prud'homme (IRMA, Strasbourg)
  • Paul Zimmermann (INRIA/LORIA, Nancy)