RFR: 8341470: BigDecimal.stripTrailingZeros() optimization [v44]

[Raffaello Giulietti]

On Thu, 17 Oct 2024 14:51:28 GMT, fabioromano1 <duke at openjdk.org> wrote:

>> OK, let me reformulate the reasoning to check that we are in sync.
>> For simplicity, I'm assuming that the powers of 2 are _not_ stripped away, so I'm using powers of 10 rather than powers of 5. Adding the powers of 2 optimization to the reasoning is then straightforward.
>> 
>> As above, let v0, z0 and s0 be the initial values at method entry of intVal, z and scale, resp.
>> We need to return intVal = v0 / 10^z0, scale = s0 - z0.
>> 
>> Let sexp be the running sum of all exponents exp inside both loops that lead to zero remainders in the division intVal / 10^exp.
>> It should be easy to see that both "then" branches maintain
>> 
>> z = z0 - sexp, intVal = v0 / 10^sexp, scale = s0 - sexp
>> 
>> and that both branches in both loops maintain
>> 
>> remainingZeros >= z
>> 
>> When the 2nd loop exits, remainingZeros = 0, so z = 0. This means z0 = sexp, intVal = v0 / 10^z0, scale = s0 - z0 (correctness).
>> 
>> In addition, both loops exit for the reasons in the comments (termination) and both loops require very few iterations (quality of service).
>
> @rgiulietti That's correct, although I prefer that the correctness is proved by "reducing the size of the problem" rather than "total number of removed powers", because it was the logic to prove implicitly the correctness of the older implementation, namely by reducing the number of zeros without exceeding the largest scale decreasing allowed, and because, at least for me, it is less complex to write and understand.

With the definition remainingZeros = scale - preferredScale, the proof above could be adapted almost on the fly to the old implementation.

In any reduction approach, you still need to prove that the reduced problem is equivalent to the original. This is to say that the running variables (in code and proof) must somehow be related to the initial values.

Anyway, very nice contribution! Thanks.

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

PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1804972052