RFR: 4511638: Double.toString(double) sometimes produces incorrect results [v2]

[Raffaello Giulietti]

On Fri, 16 Apr 2021 11:30:32 GMT, Raffaello Giulietti <github.com+70726043+rgiulietti at openjdk.org> wrote:

>> Hello,
>> 
>> here's a PR for a patch submitted on March 2020 [1](https://cr.openjdk.java.net/~bpb/4511638/webrev.04/) when Mercurial was a thing.
>> 
>> The patch has been edited to adhere to OpenJDK code conventions about multi-line (block) comments. Nothing in the code proper has changed, except for the addition of redundant but clarifying parentheses in some expressions.
>> 
>> 
>> Greetings
>> Raffaello
>
> Raffaello Giulietti has updated the pull request incrementally with one additional commit since the last revision:
> 
>   4511638: Double.toString(double) sometimes produces incorrect results

Hello,

thanks for reading my writing.

In some way, Ryu and Schubfach are similar in the sense that both are based on the observation that good, fixed size approximations of powers of 10 lead to extremely efficient algorithms. Both algorithms end up with a lookup table of 617 approximations.

The proof of the central theorem of Schubfach is based on continued fractions. It was prepared on ACL2 by the late Dmitry Nadezhin, who was a member of Oracle's formal verification group. Dmitry also knew my writing inside-out: not a formal peer review but perhaps even more insightful.

Schubfach has been exhaustively tested on all 2^32 floats, with approximations of powers of 10 of 63 bits each, rather than the full 126 bits used for doubles (the minimum size for doubles is 123 bits).
It has also been tested for months on doubles, accumulating several trillions of witnesses and no failure.
The exhaustive test on floats is an optionally executed part of the contributed code.
After more than 25 years the current JDK implementation still contains anomalies, so I guess it isn't tested as well as Schubfach.

A complete Schubfach conversion only depends on some dozens of primitive operations (it doesn't even need any sort of hardware division at all) and on a lookup table (fully tested for correctness in the contributed code).
The current implementation in the JDK relies on the correctness of BigInteger and related classes, which are way more complex to thoroughly test and to be confident upon.

Checking whether the 617 tabulated powers of 10 are very close to powers of 2 would be very easy, so I'm not sure I understand your point.
Identifying the hard cases would require even more theory and would be an endeavor in itself. This theory could, in turn, contain small errors and would probably require identifying its hard cases...

According to its author, DragonBox combines Schubfach and Grisu. AFAIK, there's no new fundamental underlying theory.
During development of Schubfach, I experimented with a similar mix: on the JVM of the time (2018) performance was worse than pure Schubfach and the code more complex, so I gave up and switched back to the simpler design, which C2 likes better.


Greetings
Raffaello

-------------

PR: https://git.openjdk.java.net/jdk/pull/3402