École thématique PRECIS
Du 25 au 29 mars 2013
Fréjus
40 places disponibles
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.
lundi 25/03
14:00 15:30
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:00Pause
16:00 19:00Arithmé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:30Arithmé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:00Pause
11:00 12:30Arithmétique flottante en précision arbitraire (suite)
Vincent Lefèvre (INRIA Grenoble - Rhône-Alpes / LIP, ENS-Lyon)
Suite12:30 14:00Repas
14:00 15:30
Arithmétique stochastique
Fabienne Jézéquel et Jean-Luc Lamotte (LIP6)
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:00Pause
16:00 17:30Arithmétique stochastique (suite)
Fabienne Jézéquel et Jean-Luc Lamotte (LIP6)
Suitemercredi 27/03
09:00 10:30Conception 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)
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:00Pause
11:00 12:30Conception 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)
Suite12:30 14:00Repas
14:00 15:30Conception 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)
Suite15:30 16:00Pause
16:00 17:30Conception 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)
Suitejeudi 28/03
09:00 10:30Arithmétique flottante par intervalles
Nathalie Revol (Inria, ENS de Lyon, LIP) et Philippe Théveny (ENS de Lyon, LIP)
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:00Pause
11:00 12:30Arithmétique flottante par intervalles
Nathalie Revol (INRIA, ENS de Lyon, LIP) et Philippe Théveny (ENS de Lyon, LIP)
Suite12:30 14:00Repas
14:00 15:30La 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:00Pause
16:00 17:30Lepton
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:30Sumatra
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:00Pause
11:00 12:30La 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:00Repas
- 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)
- 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)
Sommaire
