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

Joseph D. Darcy Joe.Darcy at Sun.COM
Tue Dec 15 19:16:34 UTC 2009

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 .


> 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 

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



More information about the core-libs-dev mailing list