École Calcul Numérique Certifié
[official page]
Supports de cours.
Contexte.
Cette école est organisée dans le cadre
des écoles CEA-EDF-INRIA, sous la coordination de
Luc Bouganim pour les écoles d'informatique.
Les organisateurs scientifiques sont
Fabrice Rouillier
et Paul Zimmermann.
Date et lieu.
Cette école aura lieu au
LORIA (Nancy), les 25 et 26 octobre 2007.
Public visé.
Ingénieurs ou chercheurs, du domaine public ou privé.
Nombre de participants.
Le nombre de participants minimal
est 10 personnes, et maximal 20 personnes.
Description.
Le but de cette école est de sensibiliser aux problèmes
posés par les calculs numériques via l'utilisation
d'arithmétique flottante (erreur d'arrondi, précision limitée,
débordement de capacité, etc.)
et de proposer quelques
outils innovants sur ce thème, avec en particulier une
formation à la bibliothèque MPFR
de calcul flottant en précision arbitraire.
Contrairement aux calculs entiers, les calculs sur des nombres flottants sont
par nature inexacts. Il est donc primordial de contrôler a priori ou a
posteriori les erreurs d'arrondi effectuées dans un calcul donné, et cela
indépendamment des possibles erreurs de méthode dues au schéma numérique
utilisé (maillage, approximation polynomiale, troncature). Nous présenterons
plusieurs solutions permettant de contrôler ces erreurs d'arrondi (arithmétique
d'intervalles, précision arbitraire, méthodes stochastiques, etc.). Parmi ces
outils, nous mettrons l'accent sur la bibliothèque MPFR.
L'objectif est qu'à la fin de l'école, les participants aient acquis
le b-a-ba leur permettant de maîtriser par eux-mêmes MPFR,
pour résoudre leurs vrais problèmes, via
des travaux pratiques sur machine, pour une prise en main
effective de cette bibliothèque, et la résolution de problèmes
jouets.
L'école comprend aussi une session ouverte,
dont l'objectif est
d'utiliser MPFR sur de vrais problèmes rencontrés par les
participants dans leur travail d'ingénieur ou de chercheur.
(Les participants sont vivement invités à apporter de tels problèmes,
éventuellement communiqués à l'avance aux organisateurs.)
Programme :
- Jeudi 25 octobre :
- 10h00 Accueil des participants et café de bienvenue
- 10h30 Présentation générale du thème calcul flottant (Guillaume Hanrot,
LORIA/INRIA Lorraine).
Résumé :
l'introduction des nombres flottants obéit à une remarque simple : il n'est pas
possible de représenter sur ordinateur tous les nombres réels. Plus que pour
les entiers, ce constat élémentaire pose des problèmes délicats, si l'on veut
préserver les principales propriétés des réels. Nous présenterons le principal
paradigme du calcul flottant, la norme IEEE-754, puis nous décrirons les
différents outils disponibles et leur limites.
- 11h30 Présentation de la bibliothèque MPFR (Paul Zimmermann,
LORIA/INRIA Lorraine).
Résumé : cet exposé fera une présentation générale de la
bibliothèque MPFR de calcul flottant en précision arbitraire.
On détaillera son domaine d'application, ses limites, et son originalité
par rapport aux autres bibliothèques de calcul flottant (arrondi
correct, précision au bit près, exceptions).
L'exposé expliquera comment l'exigence d'arrondi correct est
obtenue, et évoquera les algorithmes utilisés par MPFR.
Enfin, quelques applications utilisant cette bibliothèque seront
présentées.
- 12h30 Déjeuner
- 14h00 Premiers pas avec MPFR (Vincent Lefèvre, LIP/INRIA Rhône-Alpes).
Résumé :
Les participants écriront leurs premiers programmes utilisant
la bibliothèque MPFR, à l'aide d'exercices simples, dont les
solutions seront commentées (travaux pratiques sur machine).
Les spécificités de MPFR seront abordées, comme les différents
modes d'arrondi (par exemple pour calculer des bornes d'erreur
certifiées) et la possibilité de fixer indépendamment la
précision de chaque variable pour effectuer plus rapidement
certains calculs nécessitant peu de précision.
- 16h00 Pause café
- 16h30 Travaux pratiques (suite)
- 18h00 Fin de la journée
- 20h00 Dîner au Grand
Café Foy, sur la célèbre place Stanislas
- Vendredi 26 octobre :
- 09h00 Analyse statique de la précision de programmes faisant intervenir
des nombres flottants (Sylvie Putot, CEA)
Résumé : Dans cette présentation, j'exposerai les principes de l'analyseur
FLUCTUAT de la précision de calculs faisant intervenir des nombres
flottants, et l'intérêt de l'utilisation de MPFR pour son implémentation.
Prenant un programme C et un ensemble de valeurs possibles
pour ses entrées ou paramètres, FLUCTUAT calcule pour chaque variable,
un encadrement garanti de l'ensemble de ses valeurs possibles en fin
du programme, ainsi que de l'erreur due aux arrondis successifs.
D'autre part, il décompose cette erreur selon sa provenance dans le
programme C analysé, de façon à indiquer les points du programme dont
proviennent les imprécisions les plus importantes.
On réalise pour cela une abstraction des calculs effectués
par le programme, basée sur l'arithmétique affine. Je montrerai en
particulier
comment l'utilisation de la bibliothèque MPFR permet une implémentation
sûre et précise de cette abstraction dans FLUCTUAT.
- 10h00 Pause café.
- 10h30 Travaux pratiques (suite)
- 12h30 Déjeuner
- 14h00 Session ouverte (problèmes apportés par les participants)
- 16h00 Pause café
- 16h30 Fin de l'école