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

[Ulf Adams]

Very cool!

On Fri, Sep 28, 2018 at 5:15 PM Dmitry Nadezhin <dmitry.nadezhin at gmail.com>
wrote:

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

I believe that my minmax proof applies to Raffaello's algorithm as well,
and I get slightly tighter bounds (124 vs. 126). I have some
work-in-progress to find even tighter bounds, though I'm not sure yet if it
will work out. I found a method to compute a counter-example if there
aren't enough bits, but I'm not sure whether it's exhaustive (whether it's
guaranteed to find a counter-example if one exists). It doesn't make a
difference in this case, as long as it's <= 128 bits (or maybe < 128 to
avoid overflow in some cases).


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