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

Joseph D. Darcy Joe.Darcy at Sun.COM
Mon Dec 14 23:31:58 UTC 2009

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


More information about the core-libs-dev mailing list