Dilemme du Fabricant de Tables – TaMaDi

B.1.2.1 Calcul des HR-points

Pour localiser les HR points d’une fonction, il faut tout d’abord approcher cette fonction par un polynôme. Le faire de manière garantie, c’est-à-dire en donnant une borne à la fois fine et certaine sur l’erreur d’approximation a fait l’objet de la thèse de Mioara Joldes. Suivant le degré du polynôme, le domaine dans lequel cette approximation est valide est plus ou moins grand.

Ensuite, deux classes de méthodes peuvent être utilisées :
- pour des polynômes de degré 1, le L-Algorithme, développé dans la thèse de Vincent Lefèvre ;
- pour des polynômes de plus grand degré, l’algorithme SLZ, proposé par Stehlé, Lefèvre et Zimmermann.

Nous avons travaillé sur la parallélisation sur GPU du L-algorithme, ainsi que sur l’adaptation à de très grandes précisions de l’algorithme SLZ.

B.1.2.2 Validation des résultats fournis

Notre but était de fournir, en même temps que des HR-points, un certificat, testable par un assistant à la preuve tel que Coq, garantissant la validité des calculs qui ont mené à l’obtention de ces HR-points. Notre travail a essentiellement porté sur deux points :

- la validation des approximations polynomiales utilisées (c’est l’objet du sous-projet « CoqApprox » ) ;
- la validation (en faisant appel à une formalisation du Lemme de Hensel) des solutions fournies par l’algorithme SLZ (c’est l’objet du sous projet « CoqHensel »)

Deux bibliothèques Coq, CoqApprox (http://tamadi.gforge.inria.fr/CoqApprox/) et CoqHensel (http://tamadi.gforge.inria.fr/CoqHensel/) permettent de valider les HR points fournis. Coq Approx dépasse très largement les objectifs initiaux et est susceptible d’être utile à tous ceux qui veulent garantir des approximations polynomiales de fonctions. La chaîne de génération de certificats pour les HR points fonctionne et a été validée sur quelques exemples.

La parallélisation sur GPU du L-algorithme, réalisées par l’équipe Pequan, ainsi qu’une modification de cet algorithme, présentée dans la thèse de Mourad Gouicem ont permis d’obtenir des facteurs d’accélération impressionnants (la nouvelle implantation est environ 50 fois plus rapide). Ceci va permettre de très vite publier de nouveaux HR points.

Plusieurs récompenses ont été obtenues par les membres du projet : le « best paper award » de la conférence ASAP 2011 pour l’article An FPGA architecture for solving the Table Maker's Dilemma ; la médaille d’argent du CNRS en 2013 pour Jean-Michel Muller ; le Prix La Recherche 2013 pour les Sciences de l’Information pour l’article On the computation of correctly-rounded sums.

Le projet TaMaDi permet de construire des HR-cas certifiés pour les fonctions transcendantes usuelles. Ceci permettra de garantir que certaines bibliothèques de calcul de ces fonctions produisent toujours un arrondi correct, ce qui était recommandé par le standard virgule flottante IEEE 754-2008. En cela, le projet va avoir des conséquences importantes sur la qualité et la prouvabilité de programmes numériques.

- 4 articles dans des journaux internationaux
- 1 chapitre de livre
- 9 communications à des conférences internationales avec actes publiés
- 3 thèses de doctorat
- 3 conférences invitées
- 2 logiciels:
The CoqApprox library: rigorous polynomial approximation using Taylor models inside the Coq proof assistant – présenté à NFM 2012 – Disponible à l’adresse tamadi.gforge.inria.fr/CoqApprox/

The CoqHensel library: effective certificate checkers based on Hensel's lemma inside the Coq proof assistant. Disponible à tamadi.gforge.inria.fr/CoqHensel/coqhensel-1.0.0-coqdoc/toc.html

En arithmétique virgule flottante (VF), avoir des opérations complètement spécifiées est une exigence-clé, si on veut développer du logiciel portable au comportement prévisible. Depuis 1985, les quatre opérations arithmétiques sont spécifiées (elles doivent être correctement arrondies: le système doit renvoyer le nombre VF le plus proche du résultat exact). Ce n'est pas tout-à-fait le cas pour les fonctions mathématiques de base: la même fonction pourra renvoyer des résultats significativement différents suivant l'environnement, avec 2 conséquences pour les logiciels utilisant ces fonctions:
- il est presque impossible d'estimer leur précision
- leur portabilité est délicate à garantir
Ce manque de spécification est dû à un problème appelé le Dilemme du fabricant de tables. Pour calculer f(x) dans un format donné, on calcule une approximation de f(x) qu'on arrondit au nombre VF le plus proche. Le problème est: quelle doit être la précision de l'approximation pour que le résultat obtenu soit toujours égal à f(x) arrondi au plus proche nombre VF?
Pour résoudre ce problème, on doit déterminer, pour chaque format & fonction considérés quel est le point le plus dur à arrondir (HR-point), i.e., le nombre VF tel que f(x) est le plus proche du milieu de 2 nombres VF consécutifs. La manière naïve de résoudre ce problème (recherche exhaustive) est impraticable. Ce projet vise à fournir:
- pour les formats et fonctions les plus courants, des tables de HR-points, avec des preuves de leur correction
- du code open-source permettant de trouver les HR-points pour d'autres formats & fonctions
Obtenir ces points permettra de construire des bibliothèques de fonctions très efficaces, permettant une spécification complète des fonctions usuelles en arithmétique VF, avec des conséquences à terme sur la portabilité et la qualité des logiciels numériques.
L'état de l'art se résume comme suit:
- en 1991, IBM a lancé une bibliothèque, libultim, maintenant abandonnée, clamant être avec arrondi correct. Sans connaissance des HR-points, les concepteurs surestimaient la précision intermédiaire nécessaire, donnant ainsi de piètres performances
- l'équipe Arénaire (une des proposantes de ce projet) et l'équipe CACAO du LORIA ont conçu des algorithmes (L-algorithme et algorithme SLZ) et publié des HR-points pour quelques fonctions en double précision. La complexité de leurs méthodes est exponentielle en le nombre de bits du format: elles ne peuvent être utilisées avec des formats significativement supérieurs à la double précision.
- ces dernières années, Arénaire a développé une bibliothèque, CRLibm, qui implante les principales fonctions en faible précision. L'arrondi correct est fourni avec un surcoût négligeable. Ces performances ont conduit le comité de révision de la norme IEEE 754 à recommander (sans imposer) l'arrondi correct pour certaines fonctions mathématiques. Le standard IEEE 754-2008 a été adopté en 2008.
Nos méthodes ne peuvent être utilisées en grande précision. Et pourtant, IEEE 754-2008 spécifie des formats décimal et binaire 128 bits. de plus le processus de construction de nos HR-points est long et complexe, ce qui jette un doute sur les résultats fournis. On doit donc complètement reconsidérer les méthodes utilisées, en se focalisant sur 3 aspects:
- grosses précisions: on doit construire de nouveaux algorithmes pour les formats supérieurs à la double-précision
- preuve formelle: on doit fournir des preuves formelles des parties critiques de nos méthodes
- calcul agressif: les méthodes conçues jusqu'ici demandent des semaines de calcul sur des centaines de PC. Même si on améliore les algorithmes, pour traiter de plus gros formats on doit étudier divers moyens de massivement paralléliser les calculs
On vise à des résultats pratiques: tables de HR points, programmes pour les calculer, preuves de leur correction, avec pour conséquence des librairies de fonctions plus rapides et fiables.