Code review request for 6908131 Pure Java implementations of StrictMath.floor(double) &StrictMath.ceil(double)

[Joseph D. Darcy]

Dmitry Nadezhin wrote:
> > The current specification of the "interesting" methods in 
> StrictMath, such as sin/cos, log, > etc. are to use the FDLIBM 
> algorithms.
>
> Thank you. I forgot about these lines in java.lang.StrictMath .

[snip]

> As specification of java.lang.StrictMath is in terms of reference 
> fdlibm C library
> and algorithms in new java.lang.StrictMath are expected similar to 
> fdlibm algorithms,
> the task of formal verification becomes easier.
>
> The comment 3 in fdlibm's readme file warns about
> ---
>   3. Compiler failure on non-standard code
>   Statements like
>               *(1+(int*)&t1) = 0;
>   are not standard C and cause some optimizing compilers (e.g. GCC)
>   to generate bad code under optimization.    These cases
>   are to be addressed in the next release.
> ---
> Nevertheless, I hope that for some additional assumptions about C 
> pointers, the meaning
> of fdlibm C code can be used as the specification.

The C language does not really define an operational semantics for these 
operations.  In contrast, with the tighter specification of Java's 
integral and floating-point types and expressions using those values, it 
is really well-posed to discuss the meaning of Java versions of these 
algorithms.

> However, there is a question. Many methods of java.lang.StrictMath are
> used in a reference implementation of java.lang.Math methods.
> java.lang.Math specifies methods in terms of accuracy of the returned 
> result
> and monotonicity of the methods.
> Suppose that there is still a bug in fdlibm 5.3 and some fdlibm 
> function fails to
> satisfy one ulp accuracy or monotonicity. What will be the 
> specification of
> corresponding java.lang.StrictMath method in such a case ?

The FDLIBM functions are believed to follow the stated quality of 
implementation criteria in java.lang.Math.  When that turns out not to 
be the case, there are a variety of remedies including fixing the bug in 
FDLIBM.  Fixing bugs I had independently found in pow and tan prompted 
raising the required FDLIBM version from 5.2 to 5.3, see 5033578 "Java 
should require use of latest fdlibm 5.3."

Cheers,

-Joe