Blanc SIMI 2 - Sciences de l'information, de la matière et de l'ingénierie : Sciences de l’information, simulation

Table Maker's Dilemma – TaMaDi

TaMaDi: The Table Maker's Dilemma

Solving the Table Maker's Dilemma to get more accurate functions

General goals of the project

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 are IEEE specified (it is required that they should be correctly rounded). 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:<br /><br />• it is difficult to estimate their accuracy;<br />• their portability is difficult to guarantee.<br /><br />The lack of specification (partly solved in the recent IEEE 754-2008 standard for FP arithmetic) is due to a problem called the Table Maker’s Dilemma (TMD). To compute f(x) in a given format, 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 floating-point format and for each function f , the hardest to round (HR) points, that is, the FP numbers x such that f (x) is closest to the exact middle of two consecutive FP numbers. The naive method of finding these points is far too impractical. The major goal of the project was :<br /><br />• for the most common formats and functions, tables of HR-points, with proofs of their correction ;<br />• open-source code that allows one to find HR-points for other formats and functions.<br /><br />Obtaining these points makes it possible to design efficient function libraries. This in turn allows for a complete specification of the usual functions in FP arithmetic, with long-term consequences on the portability and quality of numerical software.<br />

B.2.2.1 Computation of the HR points

To find the HR points of a function, one must first approximate that function by a polynomial. Doing that in a guaranteed manner, i.e., with a tight and certain bound on the approximation error was the topic of Mioara Joldes’ PhD thesis. The size of the domain in which the approximation is valid depends on the degree of the polynomial.

Then, two classes of methods can be used :
• for degree-1 polynomials, the L-Algorithm, developed in Vincent Lefèvre’s PhD dissertation ;
• for polynomials of higher degree, the SLZ algorithm, intriduced by Stehlé, Lefèvre, and Zimmermann.

We have worked on the parallelization (on GPU) of the L-Algorithm, and on the adaptation of SLZ to big precisions.

B.2.2.2 Validation of the obtained results

Our goal was to provide, along with HR-points, a certificate, checkable by a proof assistant such as Coq, that would guarantee the validity of the chain of calculations that generated the HR-points. Our work mainly focussed on two issues :
• The validation of the polynomial approximations (subproject « Coq Approx » ;
• The validation (using a formalization of Hensel’s Lemma) of the solutions provided by the SLZ algorithm (subproject « Coq Hensel »)

Two Coq Libraries, Coq Approx (http://tamadi.gforge.inria.fr/CoqApprox/) and Coq Hensel (http://tamadi.gforge.inria.fr/CoqHensel/) make it possible to validate the computed HR points. It is worth being noticed that Coq Approx goes far beyond the initial goals and can be useful to anybody who wants to guarantee polynomial approximations. The chain that generates certificates for HR points works and has been checked on some examples.

The parallelization and GPU implementation of the L-Algorithm, done by the PEQUAN team, along with a modification of that algorithm presented in Mourad Gouicem’s PhD dissertation allowed us to get impressive acceleration factors (the new implementation is 50 times faster). This will make it possible to publish new HR points very soon.

Several awards have been given to project members : the Best paper award of the ASAP’2011 conference for the article An FPGA architecture for solving the Table Maker's Dilemma ; the CNRS Silver Medal given to Jean-Michel Muller ; the La Recherche 2013 Prize for Computer Science for the paper On the computation of correctly-rounded sums.

The TaMaDi project lows to compute certified HR-points for the usual transcendental functions. This will allow to guarantee that elementary function libraries will always return correctly rounded results, as was recommended by the IEEE 754-2008 standard. In the long-run, this will have an influence on the quality and provability of numerical software.

- 4 articles in international journals
- 1 book chapter
- 9 communications to international conferences with published proceedings
- 3PhD dissertations
- 3 invited conferences
- 2 software libraries:
The CoqApprox library: rigorous polynomial approximation using Taylor models inside the Coq proof assistant, Available at tamadi.gforge.inria.fr/CoqApprox/

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

In floating-point (FP) arithmetic, having fully-specified operations is a key-requirement, if one wants portable and predictable numerical software. Since 1985, the four arithmetic operations are specified (they must be correctly rounded: the system must return the FP number nearest the exact result). This is not fully the case for the basic mathematical functions. The same function may return significantly different results depending on the environment. Hence, numerical programs using these functions suffer from various problems:
• it is almost impossible to estimate their accuracy;
• their portability is difficult to guarantee.
The lack of specification is due to a problem called the Table Maker’s Dilemma. To compute f(x) in a given format, where x is a FP number, we first compute an approximation to f(x) and then we round it to the nearest FP number. The problem is: what must the accuracy of the approximation be to ensure that the obtained result is always equal to f(x) rounded to the nearest FP number?
To solve that problem, we must locate, for each considered FP format & function, what is the hardest to round (HR) point, i.e., the FP number x such that f (x) is closest to the exact middle of two consecutive FP numbers. The naive way of finding it (evaluating f at each FP number) is by far impractical. This project aims at providing
• for the most common formats & functions, tables of HR points, with proofs of their correctness;
• open source software that allows one to compute HR points for other functions & formats.
Getting these points will allow for very efficient math function libraries, leading the path to a full specification of the usual functions in FP arithmetic, with long-term consequences on the quality and portability of numerical software.
The state-of-the art can be summarized as follows:
• In 1991, IBM released a library, libultim, now abandoned, that claimed correct rounding in double-precision. Since this was done without knowledge of the HR points, the necessary precision for the intermediate calculation was overestimated, resulting in poor performance;
• the Arénaire team (one of the applicants) and the CACAO team of LORIA (Nancy) have designed algorithms, and obtained & published HR points for some functions in double precision. The complexity of their methods is exponential with the number of bits of the format, so that they cannot be applied to formats significantly larger than double precision;
• in the last years, using the obtained HR points, Arénaire developed a library, CRLibm , that implements the most common functions in double precision. It offers code where the cost of correct rounding is negligible. These performances led the IEEE-754 revision committee to recommend (yet does not
impose) correct rounding for some functions. The new 754-2008 standard for FP arithmetic was adopted in 2008.
Our methods cannot be used in large precisions. And yet, IEEE 754-2008 specifies 128-bit binary & decimal formats. Also, the processes that generate our HR cases are based on complex and long calculations that cast some doubt on the correctness on the results. Hence, we need to fully reconsider the methods used to get HR points, and focus on 3 aspects:
• large precisions: we must get new algorithms for dealing with precisions larger than double. ;
• formal proof: we must provide formal proofs of the critical parts of our methods.
• aggressive computing: the methods we have designed so far require weeks of computation on hundreds of PCs. Even if we design faster algorithms, to deal with larger formats we must consider various ways of massively parallelizing them.
We aim at getting practical results: tables of HR points, programs for getting them, formal proofs of their correctness, with as a consequence faster and better mathematical function programs.

Project coordination

Jean-Michel MULLER (INRIA Ctre Grenoble Rhone-Alpes) – Jean-Michel.Muller@ens-lyon.fr

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.

Partner

Pequan-LIP6 UNIVERSITE PARIS VI [PIERRE ET MARIE CURIE]
INRIA INRIA - Centre Sophia-Antipolis
INRIA Rhône-Alpes-EPI ARENAIRE INRIA Ctre Grenoble Rhone-Alpes

Help of the ANR 418,033 euros
Beginning and duration of the scientific project: - 36 Months

Useful links

Explorez notre base de projets financés

 

 

ANR makes available its datasets on funded projects, click here to find more.

Sign up for the latest news:
Subscribe to our newsletter