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

[Dmitry Nadezhin]

I would like to tell about some steps towards formal check of Raffaello's
human proof.
I work on formal verification of some Oracle projects but they are
unrelated to JDK.
In April Brian Burkhalter requested me to review the Raffaello's paper.
His paper is smart and clear but nevertheless I was afraid to miss some
possible error in his it.
So I decided to check his proofs formally. I am familiar with a proof
checker ACL2 [1]. So I used it.
ACL2 is an abbreviation of "Applicative Common Lisp". It is both a language
( a subset of Common Lisp ) and
proof assistant for reasoning about functions in this language. It is
open-source and it is developed in UT at Austin.

This work in progress can be found in this GitHub repository [2].
ACL2 definitions and proofs followed human definitions and proofs as
possible.
Materials of N-th section of the paper are in a file acl2/sectionN.lisp .
Proofs from sections 2-10 were checked by ACL2 completely.
Also cases fullCaseXS and fullCaseXM from the sections 2-11 were checked by
ACL2.
Sorry, I didn't finish formal proof of the entire paper in anticipation of
a new algorithm.

Sometimes in July a paper by Michel Hack [3] prompted us that it is
possible to avoid multi-precision arithmetic.
File acl2/cont-fractions.lisp formalizes some of Michel's ideas in ACL2.
It considers a linear mapping alpha*d from range of naturals 0 <= d <=
max-d to rationals.
It defines an algorithms which for given alpha and "max-d" returns bound
"lo" and "hi"
how non-integer results of this mapping are frar from integer grid.
If approximate computations shows that alpha*d is very close to some
integer m
m - hi < alpha * d < m + lo
then alpha * d is equal to m exactly.
Theorems frac-alpha-d-nonzero-bound-dp-correct and
frac-alpha-d-nonzero-bound-sp-correct explicitly
state bounds lo and hi for float and double Java formats.
This fact is proved using continous fractions.

Raffaello derived from this theorem that a table of powers of 5 with
126-bit precision is enough
to correctly implement DoubleToString conversion.
He designed a new implementation of DoubleToString and FloatToString and
presented it in this core-libs-dev thread.

It was exciting to know that Ulf Adama also developed fast conversion
algorithm.
New Raffaello's and Ulf's algorithms looks similar.
It would be interesting to compare them, to match similarities and to think
on differences.
For example the problem of finding "lo" and "hi" is formulated as computing
minimum and maximum of a modular product in Ilf's paper.
It would be interesting to check if our lo-hi bounds are scaled versions of
Ulf's minimum and maximum.
Ideally it would be interesting to formally verify both of them though I am
not sure if I find time for this.

If Raffaello prepares a new paper with proof of his new algorithm then I
will try to check these new proofs by ACL2 again.
I hope that paper with its formal check will increase confidence.

---

Andrew Dinn said about other problem: "how details of specific coding
operations are not always clearly
identifiable from an abstract mathematical treatment.". Formal verification
is applicable for this also.
It can be done either at Java language level or at classfile level.

Verification at classfile level requires formal model of JVM.
There are at least three models of JVM in ACL2:
i) An M5 model in the distribution of ACL2 books: [4]
ii) Defensive JVM model by CLI: [5]
iii) M6 model by Hamling Liu: [6]

Verification at Java language level can be done using other tools,
especially the KeY tool: [7].
TimSort bug [8][ has been found during to attempt to verify this
alogorithm's implementation by KeY.

Unfortunately I am not sure that I find time to verify implementation
(classfile or Java-file) of the new Raffaello algorithm.

---

[1] http://www.cs.utexas.edu/~moore/acl2/

[2] https://github.com/nadezhin/verify-todec

[3]
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8351&rep=rep1&type=pdf#page=114

[4] https://github.com/acl2/acl2/tree/master/books/models/jvm/m5

[5] http://www.computationallogic.com/software/djvm/index.html

[6] https://github.com/haliu/M6

[7] https://www.key-project.org/

[8]
http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/

On Fri, Sep 28, 2018 at 1:11 AM Brian Burkhalter <
brian.burkhalter at oracle.com> wrote:

> On Sep 27, 2018, at 9:00 AM, Raffaello Giulietti <
> raffaello.giulietti at gmail.com> wrote:
>
> > On 2018-09-27 17:53, Andrew Dinn wrote:
> >> On 27/09/18 16:37, Raffaello Giulietti wrote:
> >>   . . .
> >>> I thank you in advance for your willingness to review the code but my
> >>> understanding is that only the officially appointed reviewers can
> >>> approve OpenJDK contributions, which is of course a good policy.
> >>> Besides, as two Andrews engineers from RedHat correctly observe,
> >>> understanding the rationale of the code without the planned
> accompanying
> >>> paper is hard.
> >> Oh no, let me stop you right there! Anyone competent can offer a review
> >> (well incompetent people can too but let's assume they get ignored :-).
> >> Indeed, an expert critique is always very welcome and reviewers normally
> >> get credited even if they have no official status. The official
> >> reviewers are needed for a final say so. No one sensible is going to
> >> reject clear and clearly justified advice.
> >
> > An excellent policy, indeed!
>
> I was going to reply with essentially the same comments. While an
> imprimatur from at least one sanctioned OpenJDK reviewer is required
> eventually, comments and review from any competent parties are most
> welcome. This is especially the case for a relatively complicated topic
> such as the one of this thread.
>
> >>>> I'm not a contributor to the Jdk, and this isn't my full-time job. I
> >>>> was lurking here because I was going to send a patch for the double to
> >>>> string conversion code myself (based on Ryu).
> >>>>
> >>>
> >>> All my efforts on this projects are done in my unpaid spare time, too.
> >> Which is very much appreciated, thank you.
> >
> > Thank all of you for your interest in this issue.
>
> I would like to second that. It is great to see so many comments on this
> topic and to have knowledgable people paying attention.
>
> Brian