[Bug target/32180] Paranoia UCB GSL TestFloat libm tests fail - accuracy of recent gcc math poor

["joseph at codesourcery dot com" <gcc-bugzilla@gcc.gnu.org>]

------- Comment #22 from joseph at codesourcery dot com  2007-06-15 22:43 -------
Subject: Re:  Paranoia UCB GSL TestFloat libm tests fail
 - accuracy of recent gcc math poor

On Fri, 15 Jun 2007, rob1weld at aol dot com wrote:

> This is just one number. How many more could there be, how will you prove you
> are correct and deduce the actual correct answer in those instances. This is
> what you must answer. This is why we need a fast, simple, library that is
> accurate and comes with "proof".

You are ascribing too much significance to the proofs.  The proofs are 
proofs of bounds on the accumulation of error during the calculation 
(round-off errors and errors arising from the approximation to the 
function being used in the algorithm), not of the actual implementations 
being correct.  To go from there to the functions being correct, the 
proofs rely on:

* The tables of values / polynomial coefficients / ... used in the 
approximations must have been computed correctly.  This relies on another 
implementation (such as Maple) being correct.

* The exhaustive searches for worst cases for approximation must also have 
used another correct implementation of the functions at higher precision.

* Where the exhaustive searches haven't been able to cover the whole 
domain of the function, there must be no particularly bad problem cases 
outside the area covered.

* The C code for the functions must accurately correspond to the algorithm 
whose error bounds are proved.  Proving things directly about C code is 
hard in practice.


-- 


http://gcc.gnu.org/bugzilla/show_bug.cgi?id=32180