Re: Draft C bindings for IEEE 754-2008 part 4 now available

[Vincent Lefevre <vincent+gcc at vinc17 dot org>]

On 2014-01-07 14:36:58 +0000, Joseph S. Myers wrote:
> (As far as I know, the state of the art on exhaustive searches for
> worst cases for correct rounding - as needed to implement correctly
> rounded transcendental functions with bounded resource use - does
> not make such searches feasible for IEEE binary128, which is a clear
> reason not to require such functions to be provided.)

Well, an implementation can still provide very accurate versions
(say, with a guaranteed 512 bits accuracy), and the functions will
be correctly rounded with a very high probability. In practice, the
proof of correct rounding can be obtained only with an exhaustive
search (well there is some hope to obtain a proof if the maximum
precision of the implementation is around several thousands bits).
The exhaustive search also allows one to optimize code even more.

On 2014-01-07 14:55:31 +0000, Andrew Haley wrote:
> On 01/07/2014 02:48 PM, Joseph S. Myers wrote:
> > On Tue, 7 Jan 2014, Joseph S. Myers wrote:
> > 
> >> The IEEE 754 operations are corrected rounded.  However, the C bindings 
> > 
> > (Except that the IEEE 754 reduction operations - subclause 9.4 - return 
> > "an implementation-defined approximation".  But 9.2 is "Recommended 
> > correctly rounded functions", e.g. exp and sin, for which the strictly 
> > corresponding C functions are crexp and crsin.)
> 
> Has anyone found a way to do it?  Even crlibm only provides routines
> that are probably correctly rounded.  Although I'll grant you that the
> probability of incorrect rounding is very low.

For some of them, this is proved. Here's a summary of the current
status:

  http://tamadiwiki.ens-lyon.fr/tamadiwiki/images/c/c1/Lefevre2013.pdf

-- 
Vincent Lefèvre <vincent@vinc17.net> - Web: <http://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <http://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)