Main Page

From TaMaDiWiki
Revision as of 19:04, 20 September 2014 by ErikMartinDorel (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Projet ANR TaMaDi — Dilemme du Fabricant de Tables — Table Maker's Dilemma (ref. ANR 2010 BLAN 0203 01)

ANR.gif
TaMaDi.gif

Contents

Composition du projet

Équipes impliquées dans le projet/Teams involved in the project

  • Arénaire (CNRS, ENS Lyon, INRIA, UCB Lyon, Université de Lyon, Laboratoire LIP), Lyon
  • Marelle (INRIA), Sophia-Antipolis
  • Pequan (CNRS, Université Pierre et Marie Curie, Laboratoire LIP6), Paris

Porteur du projet/Project leader

Jean-Michel Muller

Membres du projet/Project members

Jean-Claude Bajard, Nicolas Brisebarre, Florent de Dinechin, Pierre Fortin, Mourad Gouicem, Stef Graillat, Guillaume Hanrot, Thibault Hilaire, Mioara Joldes, Christoph Lauter, Vincent Lefèvre, Erik Martin-Dorel, Micaela Mayero, Marc Mezzarobba, Jean-Michel Muller, Andy Novocin, Ioana Pasca, Laurence Rideau, Damien Stehlé, Laurent Théry, Serge Torres.

Publications du projet/Publications of the project: click here

Logiciels développés par les membres du projet/Software designed by project members: click here

Faits marquants de la vie du projet/Highlights

  • Mioara Joldes a soutenu sa thèse de doctorat Approximations polynomiales rigoureuses et applications le 26 septembre 2011 à l'Ecole Normale Supérieure de Lyon
  • Erik Martin-Dorel a soutenu sa thèse de doctorat Contributions to the Formal Verification of Arithmetic Algorithms le 26 septembre 2012 à l'Ecole Normale Supérieure de Lyon
  • Jean-Michel Muller a obtenu la médaille d'argent 2013 du CNRS
  • Mourad Gouicem soutiendra sa thèse de doctorat Résolution du dilemme du fabricant de tables sur architectures parallèles le 14 octobre 2013 à l'Université Pierre et Marie Curie
  • Stef Graillat soutiendra son Habilitation à Diriger des recherches Contribution à l'amélioration de la précision et à la validation des algorithmes numériques le 2 décembre 2013 à l'Université Pierre et Marie Curie

Vulgarisation/Popular science: click here

Présentation générale

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 et 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.

General overview

In floating-point (FP) arithmetic having fully-specified “atomic” operations is a key-requirement for portable, predictable and provable numerical software. Since 1985, the four arithmetic operations (+, −, ×, ÷) and the square root are IEEE specified (it is required that they should be correctly rounded: roughly speaking, the system must always return the floating-point number nearest the exact mathematical result of the operation). This is not fully the case for the basic mathematical functions (sine, cosine, exponential, etc.). Indeed, the same function, on the same variable, with the same format, may return significantly different results depending on the environment. As a consequence, numerical programs using these functions suffer from various problems. Among them:

  • it is almost impossible to estimate their accuracy (since little is known about what is returned by the imple- mented mathematical functions);
  • their portability is difficult to guarantee (a program which works on one system may be too inaccurate—or may even crash—on different systems).

The lack of specification (partly solved, thanks to our earlier work, in the recent IEEE 754-2008 standard for floating-point arithmetic) is due to a problem called the Table Maker’s Dilemma (TMD). To compute f(x) in a given format, where x is a FP number, we must first compute an approximation to f(x) with a given precision, which we round to the nearest FP number in the considered format. The problem is the following: finding what the accuracy of the approximation must be to ensure that the obtained result is always equal to the “exact” f(x) rounded to the nearest FP number. To solve that problem we have to locate, for each considered floating-point format and for each considered function f , the hardest to round (HR) points, that is, what is the floating-point numbers x such that f (x) is closest to the exact middle of two consecutive floating-point numbers (we call such a middle a breakpoint). The naive method of finding these points (evaluating the function with large precision at each floating-point number) is far too impractical.


The IEEE 754-2008 standard specifies, for instance a binary128 (“quad precision”) and a decimal128 (128-bit decimal) formats. Also, the processes that generate our HR cases are based on complex and very long calculations (years of cumulated CPU time) that inevitably cast some doubt on the correctness on their results. Hence, we need to fully reconsider the methods used to get HR points, and mainly focus on three aspects:

  • big precisions: we must get new algorithms for dealing with precisions larger than double precision. Such precisions will become more and more important (even if double precision may be thought as more than enough for a final result, it may not be sufficient for the intermediate results of a long or critical calculations);
  • formal proof: we must provide formal proofs of the critical parts of our methods. Another possibility is to have our programs generating certificates that show the validity of their results. We should then focus on proving the certificates;
  • aggressive computing: the methods we have designed for generating HR points in double precision re- quire weeks of computation on hundreds of PCs. Even if we design faster algorithms, we must massively parallelize our methods, and study various ways of doing that.

Meetings of the TaMaDi project

First meeting: Paris, September 8, 2010

Second meeting: Lyon, October 27-28, 2010

Third meeting: Sophia-Antipolis, February 22-23, 2011

Fourth meeting: Coqapprox meeting, Lyon, June 14-15, 2011

Fifth meeting: General meeting, Lyon, December 12-14, 2011

Sixth meeting: Coqapprox meeting, Lyon, July 11-12, 2012

  • Preuves formelles en Coq pour les modèles de Taylor: état actuel de la formalisation et travaux futurs, by Ioana Pasca and Erik Martin-Dorel
  • Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Deivatives, by Catherine Lelay (Proval team, Saclay)
  • Certification of inequalities involving transcendental functions using semi-definite programming, by Victor Magron
  • Validation via des opérateurs de point fixe, by Marc Mezzarobba (LIP/Arénaire)
  • Vers une formalisation du DDMF, by Assia Mahboubi
  • discussion autour du thème "Calculer en Coq avec divers niceaux de sécurité, du calcul symbolique au calcul prouvé formellement"
  • discussion sur l'orientation du code Coq (discussion spécifique au travail sur CoqApprox : séries de polynômes orthogonaux, ajout de fonctions, NaN et intervalles, récurrences, ...).

Seventh meeting: General meeting, Paris, October 18-19, 2012

Eighth meeting: Coqapprox meeting, Lyon, July 16, 2013

Final meeting, Lyon, October 7-8, 2013

Et l'après TaMaDi ?

Documentation

Download the submitted project

Public documentation on the Table Maker's Dilema

Private documentation (for project members only)

ANR.gif Inria.gif Upmc.jpg CNRS.jpg ENSL.png
TaMaDi.gif

Nous utilisons wikimedia: un peu d'aide ? un peu d'aide

Retrieved from "http://tamadiwiki.ens-lyon.fr/tamadiwiki/index.php?title=Main_Page&oldid=389"
Personal tools