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

Reply via email to