RFR: 8334755: Asymptotically faster implementation of square root algorithm [v23]

[Raffaello Giulietti]

On Fri, 12 Jul 2024 13:43:29 GMT, fabioromano1 <duke at openjdk.org> wrote:

>> src/java.base/share/classes/java/math/MutableBigInteger.java line 1941:
>> 
>>> 1939: 
>>> 1940:             // Initial estimate is the square root of the unsigned long value.
>>> 1941:             long s = (long) Math.sqrt(x > 0 ? x : x + 0x1p64);
>> 
>> As a matter of simplification, the above cases can be collapsed to just this one. I don't think there's a real need to optimize for 0, [1, 4), `int`.
>> 
>> Also, there should be a proof that the code below is correct, as there are many roundings involved.
>> 
>> Suggestion:
>> 
>>             long s = (long) Math.sqrt(x >= 0 ? x : x + 0x1p64);
>
> The proof has been made simply by exaustive experiment: for every long value `s` in [0, 2^32) such that `x == s * s`, it is true that `s == (long) Math.sqrt(x >= 0 ? x : x + 0x1p64)`. This can be verified directly by a Java program.
> It means that Math.sqrt() returns the correct value for every perfect square, and so the value returned by Math.sqrt() for whatever long value in the range [0, 2^64) is either correct, or rounded up by one if the value is too high and too close to a perfect square.

(Yes, I proved it to myself in this way.)

A similar explanation should be in a comment in the code, not here. The source of truth is the code, not the comments on GitHub ;-)

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

PR Review Comment: https://git.openjdk.org/jdk/pull/19710#discussion_r1675959960