Code review request for 6908131 Pure Java implementations of StrictMath.floor(double) &StrictMath.ceil(double)
Dmitry Nadezhin
Dmitry.Nadezhin at Sun.COM
Tue Dec 15 06:08:16 UTC 2009
> 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 .
* <p>To help ensure portability of Java programs, the definitions of
* some of the numeric functions in this package require that they
* produce the same results as certain published algorithms. These
* algorithms are available from the well-known network library
* {@code netlib} as the package "Freely Distributable Math
* Library," <a
* href="ftp://ftp.netlib.org/fdlibm.tar">{@code fdlibm}</a>. These
* algorithms, which are written in the C programming language, are
* then to be understood as executed with all floating-point
* operations following the rules of Java floating-point arithmetic.
*
* <p>The Java math library is defined with respect to
* {@code fdlibm} version 5.3.
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.
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 ?
Joseph D. Darcy wrote:
> Dmitry Nadezhin wrote:
>> Joseph D. Darcy wrote:
>>> Yes, porting FDLIBM to Java has been an oft-delayed "nice to have"
>>> project of mine. It is not obvious from looking at my ceil/floor
>>> code, but it started with the FDLIBM versions of those algorithms.
>>> The tests are new and greatly outnumber the code changes, as it
>>> typical in this line of work :-) I think getting an all-java
>>> StrictMath library would be best done as a series of small batches
>>> so floor/ceil could be a start.
>> Floating-point algorithms are difficult to test.
>> Maybe, the new StrictMath.java can be verified by formal methods (in
>> addition to tests) ?
>> We would be more confident, if we obtain machine-checked proof that
>> the result of method execution by JVM differs from exact mathematical
>> result no more than 1 ulp in for all Float/Double inputs.
>>
>> I googled some papers on verification of floating-point:
>> http://www-lipn.univ-paris13.fr/CerPAN/files/ARITH.pdf
>> http://shemesh.larc.nasa.gov/fm/papers/Boldo-CR-2006-214298-Floating-Point.pdf
>>
>> http://www.cl.cam.ac.uk/~jrh13/papers/fparith.pdf
>>
>> What do you think about such perspective ?
>>
>>
>
> The current specification of the "interesting" methods in StrictMath,
> such as sin/cos, log, etc. are to use the FDLIBM algorithms. Another
> approach would be to specify that "correctly rounded" algorithms be
> used. Such a specification would constrain the result according to
> the method's behavior (i.e. define a mathematically "correct" result)
> rather than defining the correct result based on matching a particular
> implementation. Developing and testing correctly rounded algorithms
> remains a research area with Jean-Michel Muller and associates doing
> good work.
>
> That said, while there is certainly value in formal methods, I think
> they would be overkill for the regression testing needs of the JDK.
>
> -Joe
More information about the core-libs-dev
mailing list