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