www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Printing floating points

reply deadalnix <deadalnix gmail.com> writes:
https://forum.dlang.org/post/r1hsv2$tt0$1 digitalmars.com

On Thursday, 6 February 2020 at 20:29:31 UTC, Walter Bright wrote:

 This one is always going to be a tough one:

 https://github.com/dlang/phobos/pull/7264

 Floating point code is extremely difficult to get right, and 
 contains a lot of very subtle traps for the unwary. (It's why 
 people are still writing research papers on formatting floating 
 point numbers.) If there's a mistake in it that subtly breaks 
 someone's floating point code, it would cause them to not trust 
 D. Just finding someone capable of reviewing it thoroughly 
 would be very difficult for any community.


While we are on this, I should point out that there has been a 
major breakthrough on the matter fairly recently called ryu.

I invite everyone who has an interest in printing floating to 
look at it. Here are a few useful links:

The original paper: 
https://dl.acm.org/doi/pdf/10.1145/3296979.3192369
Another paper: https://dl.acm.org/doi/pdf/10.1145/3360595

Source code in various languages: https://github.com/ulfjack/ryu
Jan 21 2021
next sibling parent reply Stefan Koch <uplink.coder googlemail.com> writes:
On Thursday, 21 January 2021 at 14:02:52 UTC, deadalnix wrote:

 https://forum.dlang.org/post/r1hsv2$tt0$1 digitalmars.com

 On Thursday, 6 February 2020 at 20:29:31 UTC, Walter Bright 
 wrote:

[...]


 While we are on this, I should point out that there has been a 
 major breakthrough on the matter fairly recently called ryu.

 I invite everyone who has an interest in printing floating to 
 look at it. Here are a few useful links:

 The original paper: 
 https://dl.acm.org/doi/pdf/10.1145/3296979.3192369
 Another paper: https://dl.acm.org/doi/pdf/10.1145/3360595

 Source code in various languages: https://github.com/ulfjack/ryu


I think Ilya has implemented this in mir already.
ryu is less of a breakthrough imo.
It's a modification of grisu2 (hence the name ryu (dragon in 
Japanese))
Jan 21 2021
next sibling parent jmh530 <john.michael.hall gmail.com> writes:
On Thursday, 21 January 2021 at 14:13:32 UTC, Stefan Koch wrote:

 [snip]

 I think Ilya has implemented this in mir already.
 ryu is less of a breakthrough imo.
 It's a modification of grisu2 (hence the name ryu (dragon in 
 Japanese))


Discussed here
https://forum.dlang.org/thread/yobmmccdvbmmbaolehbs forum.dlang.org
Jan 21 2021
prev sibling parent reply deadalnix <deadalnix gmail.com> writes:
On Thursday, 21 January 2021 at 14:13:32 UTC, Stefan Koch wrote:

 I think Ilya has implemented this in mir already.
 ryu is less of a breakthrough imo.
 It's a modification of grisu2 (hence the name ryu (dragon in 
 Japanese))


ryu pushes thing forward significantly, and proved it was correct 
to do so. I can't stress enough the importance of that last part, 
because there are no way you can check all possible double values 
by yourself and see if the output is correct.
Jan 22 2021
parent Walter Bright <newshound2 digitalmars.com> writes:
On 1/22/2021 5:11 AM, deadalnix wrote:

 ryu pushes thing forward significantly, and proved it was correct to do so. I 
 can't stress enough the importance of that last part, because there are no way 
 you can check all possible double values by yourself and see if the output is 
 correct.


True, but you *can* do it for float values, and the double algorithm is just 
more bits.
Jan 24 2021
prev sibling next sibling parent Berni44 <someone somemail.com> writes:
On Thursday, 21 January 2021 at 14:02:52 UTC, deadalnix wrote:

 While we are on this, I should point out that there has been a 
 major breakthrough on the matter fairly recently called ryu.


This is well known to me (I wrote PR 7264). Unfortunately ryu and
format("%f") have different goals, so ryu cannot be used there.
Anyway, I have some ideas of extending the abilities of format,
where ryu (or a similiar algorithm) might make it into phobos.
But don't expect this to happen too soon.

As far as I know, there are allready several implementations of
ryu in D available.

Berni
Jan 21 2021
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 1/21/2021 6:02 AM, deadalnix wrote:

 Source code in various languages: https://github.com/ulfjack/ryu


It's Boost licensed, yay!

Who wants to get the leet street cred for integrating this into dmd?
Jan 22 2021
parent reply Steven Schveighoffer <schveiguy gmail.com> writes:
On 1/22/21 4:33 AM, Walter Bright wrote:

 On 1/21/2021 6:02 AM, deadalnix wrote:

 Source code in various languages: https://github.com/ulfjack/ryu


 
 It's Boost licensed, yay!
 
 Who wants to get the leet street cred for integrating this into dmd?


I believe Berni44 has already made a PR for this (and did so a while ago).

Original PR: https://github.com/dlang/phobos/pull/7264 (includes a nice 
paper on what he did)

New PR: https://github.com/dlang/phobos/pull/7757

Or maybe I misunderstand what he did. I can't make heads or tails of 
this stuff.

Amaury, can you take a look at that PR?

-Steve
Jan 22 2021
next sibling parent reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Friday, 22 January 2021 at 14:02:53 UTC, Steven Schveighoffer 
wrote:

 On 1/22/21 4:33 AM, Walter Bright wrote:

 On 1/21/2021 6:02 AM, deadalnix wrote:

 Source code in various languages: 
 https://github.com/ulfjack/ryu


 
 It's Boost licensed, yay!
 
 Who wants to get the leet street cred for integrating this 
 into dmd?


 I believe Berni44 has already made a PR for this (and did so a 
 while ago).

 Original PR: https://github.com/dlang/phobos/pull/7264 
 (includes a nice paper on what he did)

 New PR: https://github.com/dlang/phobos/pull/7757

 Or maybe I misunderstand what he did. I can't make heads or 
 tails of this stuff.

 Amaury, can you take a look at that PR?

 -Steve


Interesting, doesn't seem to be ryu though
Jan 22 2021
parent reply Paul Backus <snarwin gmail.com> writes:
On Friday, 22 January 2021 at 16:42:20 UTC, Imperatorn wrote:

 Interesting, doesn't seem to be ryu though


 From the linked PDF [1]:


 Ryu and other fast algorithms have been rejected, because they 
 cannot be used for printf-like functions due to a different 
 design goal.


According to the Ryu README on Github [2], "Ryu generates the 
shortest decimal representation of a floating point number that 
maintains round-trip safety." For printf, the user is allowed to 
specify things like the precision, the field width, and whether 
leading zeros should be used for padding, so a more flexible 
algorithm is needed.

[1] 
https://raw.githubusercontent.com/berni44/printFloat/master/printFloat.pdf
[2] https://github.com/ulfjack/ryu
Jan 22 2021
parent reply deadalnix <deadalnix gmail.com> writes:
On Friday, 22 January 2021 at 18:01:41 UTC, Paul Backus wrote:

 On Friday, 22 January 2021 at 16:42:20 UTC, Imperatorn wrote:

 Interesting, doesn't seem to be ryu though


 From the linked PDF [1]:


 Ryu and other fast algorithms have been rejected, because they 
 cannot be used for printf-like functions due to a different 
 design goal.


 According to the Ryu README on Github [2], "Ryu generates the 
 shortest decimal representation of a floating point number that 
 maintains round-trip safety." For printf, the user is allowed 
 to specify things like the precision, the field width, and 
 whether leading zeros should be used for padding, so a more 
 flexible algorithm is needed.

 [1] 
 https://raw.githubusercontent.com/berni44/printFloat/master/printFloat.pdf
 [2] https://github.com/ulfjack/ryu


People have been suing variation of this for printf. But yes, it 
is not suffisient by itself.
Jan 22 2021
parent reply deadalnix <deadalnix gmail.com> writes:
On Friday, 22 January 2021 at 21:37:08 UTC, deadalnix wrote:

 People have been suing variation of this for printf. But yes, 
 it is not suffisient by itself.


Related paper: https://dl.acm.org/doi/pdf/10.1145/3360595
Jan 22 2021
parent reply Berni44 <someone somemail.com> writes:
Being the author of the PR mentioned here several times, I feel 
somewhat obliged to write something too.

On Saturday, 23 January 2021 at 00:13:16 UTC, deadalnix wrote:

 Related paper: https://dl.acm.org/doi/pdf/10.1145/3360595


That's great. I'll have a deeper look into it, whether there is 
something, that can be used for our implementation of printf.

 From first glance: It overcomes some of the speed problems I 
encountered and where I currently am trying to find something 
better. The drawback of RYU printf is the large amount of memory 
needed for the tables involved. The paper states 104KB for 
doubles (can be compressed on the expense of slowing everthing 
down). For reals it will be even more. We should make sure, that 
we do not blow up the executables more than needed. We will 
probably eventually have to decide between speed and code size - 
or we'll have to find some sort of a compromise.

On Monday, 25 January 2021 at 04:27:49 UTC, Walter Bright wrote:

 One way is to randomly generate floating point bit patterns and 
 compare the output with that of print formatting on C.


The last commit of my PR adds a test, that is doing exactly this. 
I would be happy, if people could run that test and report 
differences. (There will be some, because the snprintf 
implementations are known to contain bugs - see my comments above 
the test.)

To do so, check out the PR, uncomment the line "version = 
printFloatTest;" and run the unittests of std.format. The test 
lasts for 30 minutes (you can configure this by changing the 
value of "duration"). After that it prints some summary. (Feel 
free to change the test to make it meet your needs.)

On Monday, 25 January 2021 at 09:17:25 UTC, Ola Fosheim Grøstad 
wrote:

 You only need to test the boundary cases, so one can do this, 
 no problem.


I fear, with this approach you'll have a hard time: There are so 
many boundary cases, it's easy to miss some. - You need to test 

precision, rounding mode, different algorithms depending on the 
size of the exponent, nans, infs, subnormals, zero, 
float/double/real(s) and probably more.

On Monday, 25 January 2021 at 21:40:01 UTC, Bruce Carneal wrote:

 If I'm  wrong, if it really is as you say "no problem", then 
 the RYU author sure wasted a lot of time on the proof in his 
 PLDI 2018 paper.


There is a subtle, but important difference between proving 
correctness for RYU and printf-implementations: For RYU, the 
theorem to prove is simple to state: Find one shortest 
representation of a number, that works in round robin.

But what would be the equivalent theorem for printf? Produce the 
same result, that snprintf produces? But which implementation of 
snprintf? And what exactly does snprintf produce? Can you write 
that down? And wouldn't it make more sense to have an 
implementation that fixes the known bugs in snprintf instead of 
copying them? (For example, I read about an implementation where 
snprintf("%.2f",double.inf) produces "#J" instead of the expected 

rounded up to "J"... *lol*, or printing different results for 
identical numbers, just because one is float and the other is 
double.)

I'm not completely sure, I have not found the time to read the 
paper about RYU printf carefully, so I might be wrong, but from 
first glance I think they only prove, that the algorithm produces 
the correct digits. It ignores all the flags and stuff which make 
up about 90% of the PR.

The heart of the PR (which could be replaced by RYU printf) is 
this (version for numbers, that have no fractional part - see 
below for fractions):


 int msu = 0;
 while (msu < count - 1 || mybig[$-1] != 0)
 {


>     ulong mod = 0;
>     foreach (i;msu .. count)

     {


>         mybig[i] |= mod << 60;  // (a)
>         mod = mybig[i] % 10;    // (b)
>         mybig[i] /= 10;         // (c)
>     }
>     if (mybig[msu] == 0)
>         ++msu;
>
>     buffer[--left] = cast(byte) ('0'+mod);
> }

It's basically: Divide by 10 and print the reminder until you 
reach zero (printing from right to left). The algorithm is a 
little bit more complicated, because the numbers involved are up 
to 1000 digits long and cannot be saved anymore in a single ulong.

Going a little bit more into details here: The number which 
should be print is given in mybig[] as an integer (similar to the 
implementation of BigInt). The outer loop produces one decimal 
digit every time it is executed - the digit is saved in buffer 
(last line).

The inner loop is a division by 10 for big numbers. It is quite 
similar to a long division, like we learned it in school (here 
division by 3):

736 : 3 = 245 reminder 1.
6
-
13
12
--
  16
  15
  --
   1

First, we divide (7 / 3 = 2 reminder 1) and add another digit to 
the reminder (1 => 13) and so on. The same is done in the 
algorithm: (a) adds another digit, (b) calculates the reminder 
and (c) divides by 10. (If you worry about the reordering of the 
steps: This has the benefit, that the loop is without branch and 
therefore faster; in the first step a zero is added, which 
doesn't harm.). Finally, the last reminder is the next digit. 
(And the if below the inner loop is for speed reasons.)

As for fractional digits: Here a similar algorithm is used, but 
this time the number is multiplied each round by 10 and the 
overflow leads to the next digit.


Don't know, if this will comfort you or not, but: This algorithm 
*is* already part of Phobos since 7th of Februar 2020 and hence 
in the stable version since v2.091. It's already used for 
printing floats with %e. The PR is about adding it for %f too.
Jan 26 2021
parent reply Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
On Tuesday, 26 January 2021 at 16:25:54 UTC, Berni44 wrote:

 The paper states 104KB for doubles (can be compressed on the
 expense of slowing  everthing down).


It also notes that "the size could be halved to 52 kB with no 
performance impact".

For comparison, a simple "Hello, World!", built with 
optimizations and stripped, comes to about 700 kB.  Even allowing 
that the 128-bit table (which will support 80-bit reals) is going 
to be larger, is this really an issue on modern machines?

The only circumstances I can see it mattering is in very 
low-resource embedded use-cases where D stdlib is unlikely to be 
viable anyway.
Jan 26 2021
next sibling parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Wednesday, 27 January 2021 at 00:15:41 UTC, Joseph Rushton 
Wakeling wrote:

 On Tuesday, 26 January 2021 at 16:25:54 UTC, Berni44 wrote:

 The paper states 104KB for doubles (can be compressed on the
 expense of slowing  everthing down).


 It also notes that "the size could be halved to 52 kB with no 
 performance impact".

 For comparison, a simple "Hello, World!", built with 
 optimizations and stripped, comes to about 700 kB.  Even 
 allowing that the 128-bit table (which will support 80-bit 
 reals) is going to be larger, is this really an issue on modern 
 machines?

 The only circumstances I can see it mattering is in very 
 low-resource embedded use-cases where D stdlib is unlikely to 
 be viable anyway.


I'd vote for "overweight and almost-certainly-correct" over "trim 
but iffy" if the extra poundage is reasonable which, in the 
non-embedded environments, it appears to be.

On another note, it looks like ryu was submitted by MS in late 
2019 for inclusion in libc++.  Despite a massive 3 minutes of 
google-fuing, I'm still not sure how far that has gotten but the 
direction seems pretty clear.  A large body of others believe 
that ryu is a good way to go and are moving to standardize on it.

It's not a live-or-die issue for me but ryu looks pretty good.
Jan 26 2021
next sibling parent reply Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
On Wednesday, 27 January 2021 at 01:16:40 UTC, Bruce Carneal 
wrote:

 I'd vote for "overweight and almost-certainly-correct" over 
 "trim but iffy" if the extra poundage is reasonable which, in 
 the non-embedded environments, it appears to be.

 On another note, it looks like ryu was submitted by MS in late 
 2019 for inclusion in libc++.  Despite a massive 3 minutes of 
 google-fuing, I'm still not sure how far that has gotten but 
 the direction seems pretty clear.  A large body of others 
 believe that ryu is a good way to go and are moving to 
 standardize on it.

 It's not a live-or-die issue for me but ryu looks pretty good.


Yup, I'm in complete agreement with you on this.  I am curious if 
the MS implementation and usage carries the extra weight 
described (ryu alone is more lightweight, it's ryu printf that 
has the larger tables).
Jan 26 2021
parent reply Paul Backus <snarwin gmail.com> writes:
On Wednesday, 27 January 2021 at 01:38:38 UTC, Joseph Rushton 
Wakeling wrote:

 Yup, I'm in complete agreement with you on this.  I am curious 
 if the MS implementation and usage carries the extra weight 
 described (ryu alone is more lightweight, it's ryu printf that 
 has the larger tables).


Judging by this presentation, it's just regular Ryu:

https://www.youtube.com/watch?v=4P_kbF0EbZM
Jan 26 2021
parent Bruce Carneal <bcarneal gmail.com> writes:
On Wednesday, 27 January 2021 at 01:56:55 UTC, Paul Backus wrote:

 On Wednesday, 27 January 2021 at 01:38:38 UTC, Joseph Rushton 
 Wakeling wrote:

 Yup, I'm in complete agreement with you on this.  I am curious 
 if the MS implementation and usage carries the extra weight 
 described (ryu alone is more lightweight, it's ryu printf that 
 has the larger tables).


 Judging by this presentation, it's just regular Ryu:

 https://www.youtube.com/watch?v=4P_kbF0EbZM


This link: https://github.com/microsoft/STL/issues/172
suggests that they're adding 121KB of constant data and that 
they're compiling 385KB of source code. Wow.  Hope that's mostly 
the tables.

Also, per the youtube presentation that Paul pointed at, that 
does not include 80/128 bit FPs as their "long double" is defined 
to be "double".
Jan 26 2021
prev sibling parent reply Berni44 <someone somemail.com> writes:
On Wednesday, 27 January 2021 at 01:16:40 UTC, Bruce Carneal 
wrote:

 I'd vote for "overweight and almost-certainly-correct" over 
 "trim but iffy" if the extra poundage is reasonable which, in 
 the non-embedded environments, it appears to be.


I'd like to compare the task to write floating point numbers to 
building a car: You need a chassis, wheels, seats and other 
stuff. And you need an engine. The engine in the PR is a simple 
division by 10 (as explained above). Ryu Printf would be an other 
engine, a better one when concerned of speed only (but much worse 
in memory usage). But all else of the car would remain the same 
(and is not touched by the proof of Ryu Printf, as far as I 
know). (My plan is to start with a simple engine and replace that 
one by better ones step by step.)

Coming back to your vote, I'd say it's a vote between "overweight 
and almost-certainly-correct" vs. "trim and correct". I don't say 
that, because I'm overly self confident, but because the "engine" 
I used is quite simple. And furthermore, that simple engine is 
already part of phobos (in the %e-car) sind almost one year, I 
just reuse it for the %f-car.


 A large body of others believe that ryu is a good way to go and 
 are moving to standardize on it.

 It's not a live-or-die issue for me but ryu looks pretty good.


We are in complete agreement here. My point is: Adding ryu printf 
would be the second step before the first step: First build the 
car with a simple engine (that's what the PR does) and then 
replace this engine by a better one. I will (probably) do this 
job, but only in this order.

Adding ryu is jet another unrelated step. I've got plans to add 
ryu, or at least to prepare everything for adding it. But to do 
this std.format needs some other improvements (including 
refactoring) first, in order to add some space, where ryu nicely 

first step here, not absolutely needed, but with all these 
additions IMHO std.format is getting too large. It also 
simplifies working in parallel on replacing snprintf and 
improving the rest of std.format.
Jan 27 2021
parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Wednesday, 27 January 2021 at 08:27:13 UTC, Berni44 wrote:

 On Wednesday, 27 January 2021 at 01:16:40 UTC, Bruce Carneal 
 wrote:

 I'd vote for "overweight and almost-certainly-correct" over 
 "trim but iffy" if the extra poundage is reasonable which, in 
 the non-embedded environments, it appears to be.


 I'd like to compare the task to write floating point numbers to 
 building a car: ...


 A large body of others believe that ryu is a good way to go 
 and are moving to standardize on it.

 It's not a live-or-die issue for me but ryu looks pretty good.


 We are in complete agreement here. My point is: Adding ryu 
 printf would be the second step before the first step: First 
 build ...


I'm quite confident that I have significantly less knowledge in 
this area than you do.  Your explanations/tutorials and 
corrections are welcome.  I'm just happy to see someone working 
on an important, foundational, capability.
Jan 27 2021
parent Berni44 <someone somemail.com> writes:
On Wednesday, 27 January 2021 at 09:22:24 UTC, Bruce Carneal 
wrote:

 Your explanations/tutorials and corrections are welcome.


I added one more, going through the code in detail:

https://github.com/berni44/printFloat/blob/master/walkthrough.pdf

I hope this helps to tear down the fears somewhat...
Jan 27 2021
prev sibling parent reply "H. S. Teoh" <hsteoh quickfur.ath.cx> writes:
On Wed, Jan 27, 2021 at 12:15:41AM +0000, Joseph Rushton Wakeling via
Digitalmars-d wrote:

 On Tuesday, 26 January 2021 at 16:25:54 UTC, Berni44 wrote:

 The paper states 104KB for doubles (can be compressed on the expense
 of slowing  everthing down).


 
 It also notes that "the size could be halved to 52 kB with no
 performance impact".
 
 For comparison, a simple "Hello, World!", built with optimizations and
 stripped, comes to about 700 kB.  Even allowing that the 128-bit table
 (which will support 80-bit reals) is going to be larger, is this
 really an issue on modern machines?
 
 The only circumstances I can see it mattering is in very low-resource
 embedded use-cases where D stdlib is unlikely to be viable anyway.


If there was a way to make these tables pay-as-you-go, I'd vote for it.
Adding 104KB or 52KB even if the code never once formats a float, is not
ideal, though granted, in this day and age of cheap, high-capacity RAM
not really a big issue.


T

-- 
May you live all the days of your life. -- Jonathan Swift
Jan 26 2021
next sibling parent reply Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
On Wednesday, 27 January 2021 at 02:17:52 UTC, H. S. Teoh wrote:

 If there was a way to make these tables pay-as-you-go, I'd vote 
 for it. Adding 104KB or 52KB even if the code never once 
 formats a float, is not ideal, though granted, in this day and 
 age of cheap, high-capacity RAM not really a big issue.


Agree completely -- pay-as-you-go should be important for 
something like this.  (But then, it should be important for the 
whole stdlib...)
Jan 26 2021
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 1/26/2021 6:20 PM, Joseph Rushton Wakeling wrote:

 On Wednesday, 27 January 2021 at 02:17:52 UTC, H. S. Teoh wrote:

 If there was a way to make these tables pay-as-you-go, I'd vote for it. Adding 
 104KB or 52KB even if the code never once formats a float, is not ideal, 
 though granted, in this day and age of cheap, high-capacity RAM not really a 
 big issue.


 
 Agree completely -- pay-as-you-go should be important for something like this.
 
 (But then, it should be important for the whole stdlib...)


I've always thought things like this should be in the operating system. Get it 
right once, then everyone uses it.

Date/time/DST should be in the OS, so should the ridiculously large amount of 
code to deal with the level 3 Unicode madness.
Jan 26 2021
parent "H. S. Teoh" <hsteoh quickfur.ath.cx> writes:
On Tue, Jan 26, 2021 at 11:16:58PM -0800, Walter Bright via Digitalmars-d wrote:

 On 1/26/2021 6:20 PM, Joseph Rushton Wakeling wrote:

 On Wednesday, 27 January 2021 at 02:17:52 UTC, H. S. Teoh wrote:

 If there was a way to make these tables pay-as-you-go, I'd vote
 for it. Adding 104KB or 52KB even if the code never once formats a
 float, is not ideal, though granted, in this day and age of cheap,
 high-capacity RAM not really a big issue.


 
 Agree completely -- pay-as-you-go should be important for something
 like this.  (But then, it should be important for the whole
 stdlib...)


 
 I've always thought things like this should be in the operating
 system. Get it right once, then everyone uses it.


Or get it wrong once, and everyone rolls their own, all slightly wrong
in a different way. :-D



 Date/time/DST should be in the OS, so should the ridiculously large
 amount of code to deal with the level 3 Unicode madness.


The next best thing is to reuse a reputable library that's reasonably
widespread, like libicu.  But that adds an additional dependency, and
the API isn't always conducive to how the language works.

Reuse is hard.


T

-- 
VI = Visual Irritation
Jan 27 2021
prev sibling next sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Wednesday, 27 January 2021 at 02:17:52 UTC, H. S. Teoh wrote:

 If there was a way to make these tables pay-as-you-go, I'd vote 
 for it. Adding 104KB or 52KB even if the code never once 
 formats a float, is not ideal, though granted, in this day and 
 age of cheap, high-capacity RAM not really a big issue.


Network transfer costs responsiveness,  Web/WASM. 100Kb to do 
float to string conversion in a web app would be crazy. Same with 
embedded.

Anyway, in most system programming scenarios where you control 
the format it would be better to use hex for accuracy anyway.
Jan 26 2021
prev sibling next sibling parent Walter Bright <newshound2 digitalmars.com> writes:
On 1/26/2021 6:17 PM, H. S. Teoh wrote:

 If there was a way to make these tables pay-as-you-go, I'd vote for it.
 Adding 104KB or 52KB even if the code never once formats a float, is not
 ideal, though granted, in this day and age of cheap, high-capacity RAM
 not really a big issue.


We only really need it when the C stdlib printf is inadequate.
Jan 26 2021
prev sibling parent reply Steven Schveighoffer <schveiguy gmail.com> writes:
On 1/26/21 9:17 PM, H. S. Teoh wrote:

 
 If there was a way to make these tables pay-as-you-go, I'd vote for it.
 Adding 104KB or 52KB even if the code never once formats a float, is not
 ideal, though granted, in this day and age of cheap, high-capacity RAM
 not really a big issue.


There is a way -- dynamic libraries. It's how C does it.

But seriously, I can't imagine why we are concerned about 100KB of code 
space. My vibe.d server is 80MB compiled (which I admit is a lot more 
than I would like, but still). My phone has as much code space as 100 
computers from 10 years ago. Are you still using floppies to share D code?

-Steve
Jan 27 2021
parent reply "H. S. Teoh" <hsteoh quickfur.ath.cx> writes:
On Wed, Jan 27, 2021 at 10:18:58PM -0500, Steven Schveighoffer via
Digitalmars-d wrote:

 On 1/26/21 9:17 PM, H. S. Teoh wrote:

 
 If there was a way to make these tables pay-as-you-go, I'd vote for
 it.  Adding 104KB or 52KB even if the code never once formats a
 float, is not ideal, though granted, in this day and age of cheap,
 high-capacity RAM not really a big issue.


 
 There is a way -- dynamic libraries. It's how C does it.


That's total overkill for 100KB of data.



 But seriously, I can't imagine why we are concerned about 100KB of
 code space. My vibe.d server is 80MB compiled (which I admit is a lot
 more than I would like, but still). My phone has as much code space as
 100 computers from 10 years ago. Are you still using floppies to share
 D code?


[...]

It's not so much this specific 100KB that I'm concerned about; it's the
general principle of pay-as-you-go.  You can have 100KB here and 50KB
there and 70KB for something else, and pretty soon it adds up to
something not so small. Individually they're not worth bothering with;
together they can add quite a bit of bloat, which may be desirable to
get rid of, for embedded applications say.


T

-- 
What doesn't kill me makes me stranger.
Jan 27 2021
parent Steven Schveighoffer <schveiguy gmail.com> writes:
On 1/28/21 1:21 AM, H. S. Teoh wrote:

 On Wed, Jan 27, 2021 at 10:18:58PM -0500, Steven Schveighoffer via
Digitalmars-d wrote:

 On 1/26/21 9:17 PM, H. S. Teoh wrote:

 If there was a way to make these tables pay-as-you-go, I'd vote for
 it.  Adding 104KB or 52KB even if the code never once formats a
 float, is not ideal, though granted, in this day and age of cheap,
 high-capacity RAM not really a big issue.


 There is a way -- dynamic libraries. It's how C does it.


 
 That's total overkill for 100KB of data.


The idea is it would go into the phobos shared library, not a specific 
shared library just for floats.


 
 

 But seriously, I can't imagine why we are concerned about 100KB of
 code space. My vibe.d server is 80MB compiled (which I admit is a lot
 more than I would like, but still). My phone has as much code space as
 100 computers from 10 years ago. Are you still using floppies to share
 D code?


 [...]
 
 It's not so much this specific 100KB that I'm concerned about; it's the
 general principle of pay-as-you-go.  You can have 100KB here and 50KB
 there and 70KB for something else, and pretty soon it adds up to
 something not so small. Individually they're not worth bothering with;
 together they can add quite a bit of bloat, which may be desirable to
 get rid of, for embedded applications say.


I get that there is a need for it in niche cases. But those are very 
niche, and I'd expect a custom runtime for them anyway.

But the solution to having code that is small is to use a shared library 
for the common code. This seems like a perfect fit for that.

-Steve
Jan 29 2021
prev sibling parent reply deadalnix <deadalnix gmail.com> writes:
On Friday, 22 January 2021 at 14:02:53 UTC, Steven Schveighoffer 
wrote:

 I believe Berni44 has already made a PR for this (and did so a 
 while ago).

 Original PR: https://github.com/dlang/phobos/pull/7264 
 (includes a nice paper on what he did)

 New PR: https://github.com/dlang/phobos/pull/7757

 Or maybe I misunderstand what he did. I can't make heads or 
 tails of this stuff.

 Amaury, can you take a look at that PR?

 -Steve


I looked. i can tell you it is not ryu. I would need to dive much 
deeper into it to be confident to include this.
Jan 22 2021
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 1/22/2021 1:35 PM, deadalnix wrote:

 I looked. i can tell you it is not ryu. I would need to dive much deeper into
it 
 to be confident to include this.


One way is to randomly generate floating point bit patterns and compare the 
output with that of print formatting on C.
Jan 24 2021
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Monday, 25 January 2021 at 04:27:49 UTC, Walter Bright wrote:

 On 1/22/2021 1:35 PM, deadalnix wrote:

 I looked. i can tell you it is not ryu. I would need to dive 
 much deeper into it to be confident to include this.


 One way is to randomly generate floating point bit patterns and 
 compare the output with that of print formatting on C.


You only need to test the boundary cases, so one can do this, no 
problem.
Jan 25 2021
parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Monday, 25 January 2021 at 09:17:25 UTC, Ola Fosheim Grøstad 
wrote:

 On Monday, 25 January 2021 at 04:27:49 UTC, Walter Bright wrote:

 On 1/22/2021 1:35 PM, deadalnix wrote:

 I looked. i can tell you it is not ryu. I would need to dive 
 much deeper into it to be confident to include this.


 One way is to randomly generate floating point bit patterns 
 and compare the output with that of print formatting on C.


 You only need to test the boundary cases, so one can do this, 
 no problem.


My guess is that knowing what the actual boundary cases are is 
equivalent to having solved the original problem.  If I'm wrong, 
if it really is as you say "no problem", then the RYU author sure 
wasted a lot of time on the proof in his PLDI 2018 paper.

I also note that RYU's printf incompatibilities mentioned earlier 
in this thread seem to have been addressed.  A recent variant of 
RYU reportedly accommodates printf.
Jan 25 2021
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Monday, 25 January 2021 at 21:40:01 UTC, Bruce Carneal wrote:

 If I'm wrong, if it really is as you say "no problem", then the 
 RYU author sure wasted a lot of time on the proof in his PLDI 
 2018 paper.


Why is that? If the proof is for the algorithm then it has 
nothing to do with proving your implementation to be correct.
Jan 26 2021
parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Tuesday, 26 January 2021 at 16:31:35 UTC, Ola Fosheim Grøstad 
wrote:

 On Monday, 25 January 2021 at 21:40:01 UTC, Bruce Carneal wrote:

 If I'm wrong, if it really is as you say "no problem", then 
 the RYU author sure wasted a lot of time on the proof in his 
 PLDI 2018 paper.


 Why is that? If the proof is for the algorithm then it has 
 nothing to do with proving your implementation to be correct.


If you can construct a tractable exhaustive proof of an 
implementation, which is what I believe you asserted in this 
case, then you don't need any other proof.

I'm very happy to see the 32 bit floats done exhaustively BTW.  
It is very suggestive, but not definitive if I understand the 
problem correctly.

The mapping from the domain to the co-domain is the entire 
problem IIUC so asserting that certain ranges within the domain 
can be skipped is tantamount to saying that you know the 
implementation performs correctly in those regions.  What am I 
missing?
Jan 26 2021
next sibling parent reply John Colvin <john.loughran.colvin gmail.com> writes:
On Tuesday, 26 January 2021 at 19:02:53 UTC, Bruce Carneal wrote:

 On Tuesday, 26 January 2021 at 16:31:35 UTC, Ola Fosheim 
 Grøstad wrote:

 On Monday, 25 January 2021 at 21:40:01 UTC, Bruce Carneal 
 wrote:

 If I'm wrong, if it really is as you say "no problem", then 
 the RYU author sure wasted a lot of time on the proof in his 
 PLDI 2018 paper.


 Why is that? If the proof is for the algorithm then it has 
 nothing to do with proving your implementation to be correct.


 If you can construct a tractable exhaustive proof of an 
 implementation, which is what I believe you asserted in this 
 case, then you don't need any other proof.

 I'm very happy to see the 32 bit floats done exhaustively BTW.  
 It is very suggestive, but not definitive if I understand the 
 problem correctly.

 The mapping from the domain to the co-domain is the entire 
 problem IIUC so asserting that certain ranges within the domain 
 can be skipped is tantamount to saying that you know the 
 implementation performs correctly in those regions.  What am I 
 missing?


You can probably inductively prove - or at least become quite 
certain - that your implementation is identical to the original 
algorithm within a given set of inputs, given one good result 
within that set. What those sets look like depends on the 
algorithm of course.

E.g. given an algorithm for a function with type integer -> 
integer, if you can prove your implementation of an algorithm is 
linear w.r.t. its input and you can demonstrate it's correct for 
1, you can then infer it will be correct for any other integer 
input. I think? Off the top of my head.

Of course <insert interesting algorithm here> isn't linear w.r.t. 
its inputs, but maybe it is within some fixed subset of its 
inputs, so you only have to test one of those to cover the whole 
set. Also, linearity isn't the only property one can consider.
Jan 26 2021
parent Bruce Carneal <bcarneal gmail.com> writes:
On Tuesday, 26 January 2021 at 19:47:47 UTC, John Colvin wrote:

 On Tuesday, 26 January 2021 at 19:02:53 UTC, Bruce Carneal 
 wrote:

 On Tuesday, 26 January 2021 at 16:31:35 UTC, Ola Fosheim 
 Grøstad wrote:

 On Monday, 25 January 2021 at 21:40:01 UTC, Bruce Carneal 
 wrote:

 If I'm wrong, if it really is as you say "no problem", then 
 the RYU author sure wasted a lot of time on the proof in his 
 PLDI 2018 paper.


 Why is that? If the proof is for the algorithm then it has 
 nothing to do with proving your implementation to be correct.


 If you can construct a tractable exhaustive proof of an 
 implementation, which is what I believe you asserted in this 
 case, then you don't need any other proof.

 I'm very happy to see the 32 bit floats done exhaustively BTW.
  It is very suggestive, but not definitive if I understand the 
 problem correctly.

 The mapping from the domain to the co-domain is the entire 
 problem IIUC so asserting that certain ranges within the 
 domain can be skipped is tantamount to saying that you know 
 the implementation performs correctly in those regions.  What 
 am I missing?


 You can probably inductively prove - or at least become quite 
 certain - that your implementation is identical to the original 
 algorithm within a given set of inputs, given one good result 
 within that set. What those sets look like depends on the 
 algorithm of course.

 E.g. given an algorithm for a function with type integer -> 
 integer, if you can prove your implementation of an algorithm 
 is linear w.r.t. its input and you can demonstrate it's correct 
 for 1, you can then infer it will be correct for any other 
 integer input. I think? Off the top of my head.

 Of course <insert interesting algorithm here> isn't linear 
 w.r.t. its inputs, but maybe it is within some fixed subset of 
 its inputs, so you only have to test one of those to cover the 
 whole set. Also, linearity isn't the only property one can 
 consider.


Yes.  If we can define, with confidence, a representative set 
which spans the entire domain then we're good to go: inductive, 
piecewise, whatever.  We trade one proof (the original) for 
another (that the coverage is exhaustive/sufficient).  That can 
be a great trade but I'm not confident in my ability to define 
such a set in this case (gt 32 bit floats).  Perhaps others are 
confident.

However it goes from this point on, I'm very happy to see the 
progress made towards repeatability, towards solid foundations. 
My thanks to those hammering on this for the rest of us.
Jan 26 2021
prev sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 26 January 2021 at 19:02:53 UTC, Bruce Carneal wrote:

 If you can construct a tractable exhaustive proof of an 
 implementation, which is what I believe you asserted in this 
 case, then you don't need any other proof.


Of course you do, you need proof of the tests being correct...


 can be skipped is tantamount to saying that you know the 
 implementation performs correctly in those regions.


In general, if one understands the algorithm as implemented then 
one can either manually or automatically prove certain 
regions/ranges. Then you only need to test the regions/ranges 
that are hard to prove.

For instance, for a converter from int to string, the most likely 
failure point will be tied to crossing between "9" and "0" as 
well as the ends of the base-2 input. Meaning, if it works for 
1,2,3, you know that it also works for 4,5,6,7,8, but maybe not 
9,10.
Jan 26 2021
next sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 26 January 2021 at 20:27:25 UTC, Ola Fosheim Grøstad 
wrote:

 For instance, for a converter from int to string, the most 
 likely failure point will be tied to crossing between "9" and 
 "0" as well as the ends of the base-2 input. Meaning, if it 
 works for 1,2,3, you know that it also works for 4,5,6,7,8, but 
 maybe not 9,10.


Or to put it another way. If you can prove that these implication 
holds:

0-1 works => 2-8 works
0-11 works => 12-98 works
0-101 works => 102-998 works
etc
then you only need to test 9-11, 99-101.
Jan 26 2021
parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Tuesday, 26 January 2021 at 20:34:51 UTC, Ola Fosheim Grøstad 
wrote:

 On Tuesday, 26 January 2021 at 20:27:25 UTC, Ola Fosheim 
 Grøstad wrote:

 For instance, for a converter from int to string, the most 
 likely failure point will be tied to crossing between "9" and 
 "0" as well as the ends of the base-2 input. Meaning, if it 
 works for 1,2,3, you know that it also works for 4,5,6,7,8, 
 but maybe not 9,10.


 Or to put it another way. If you can prove that these 
 implication holds:

 0-1 works => 2-8 works
 0-11 works => 12-98 works
 0-101 works => 102-998 works
 etc
 then you only need to test 9-11, 99-101.


I think this is a great way to go for simple functions.  If the 
domain ==> co-domain mapping is truly obvious then we can exploit 
that to write an efficient unittest that we can take as the next 
best thing to the simpler exhaustive proof.

I don't see a mapping for the current problem that would allow 
for such efficient enumerative testing but it's not my field.  
Still, if/when you prove that you've fully covered the domain I'd 
be very excited to read about it.  It could be a major advance.  
Note: by "proof" I do not mean probabilistic evidence.  We 
already have that.

Even if you don't come up with proof, the attempt may be worth 
your time.  Good luck.
Jan 26 2021
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 26 January 2021 at 21:10:20 UTC, Bruce Carneal wrote:

 Even if you don't come up with proof, the attempt may be worth 
 your time.  Good luck.


Not sure what you mean... Why would anyone waste their time on 
trying to prove something for code they have no control over, it 
could change any minute, and which implementation by the way? 
*shrugs*
Jan 26 2021
parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Tuesday, 26 January 2021 at 22:23:34 UTC, Ola Fosheim Grøstad 
wrote:

 On Tuesday, 26 January 2021 at 21:10:20 UTC, Bruce Carneal 
 wrote:

 Even if you don't come up with proof, the attempt may be worth 
 your time.  Good luck.


 Not sure what you mean... Why would anyone waste their time on 
 trying to prove something for code they have no control over, 
 it could change any minute, and which implementation by the 
 way? *shrugs*


You made an assertion, in a proof discussion, that the tractable 
extension of the exhaustive proof to cover larger FP types, was 
"no problem".

Either it really is "no problem", and clarification to the good 
of all concerned would take little of your time, or you were 
mistaken and others should not expect proof level enlightenment 
from you on the topic any time soon.

It is certainly "no problem" to extend probabilistic testing but 
closing the gap between probable and proven appears to me to be 
quite a bit harder.  That's why I had hoped that you'd had a 
breakthrough.

Your inability and/or unwillingness to produce a "no problem" 
proof suggests that you have not had a breakthrough (Fermat at 
least had the excuse of dieing :-) ).

Ah well. There are a lot of other things to work on.  I just hope 
that we can come to agree on what it means to actually prove 
something.
Jan 26 2021
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Wednesday, 27 January 2021 at 00:53:11 UTC, Bruce Carneal 
wrote:

 You made an assertion, in a proof discussion, that the 
 tractable extension of the exhaustive proof to cover larger FP 
 types, was "no problem".


Eh. I argued that you can fully cover an implementation without 
doing exhaustive testing. Don't confuse what I will waste my time 
on with what is possible.

For algorithms with limited loops and limited input you can also 
fully unroll them and prove them correct by bit-blasting. 
Algorithms that are written to execute few instructions are not 
unlikely candidates for that.
Jan 26 2021
parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Wednesday, 27 January 2021 at 06:14:47 UTC, Ola Fosheim 
Grøstad wrote:

 On Wednesday, 27 January 2021 at 00:53:11 UTC, Bruce Carneal 
 wrote:

 You made an assertion, in a proof discussion, that the 
 tractable extension of the exhaustive proof to cover larger FP 
 types, was "no problem".


 Eh. I argued that you can fully cover an implementation without 
 doing exhaustive testing. Don't confuse what I will waste my 
 time on with what is possible.


No, you made an assertion regarding the tractable extension of an 
exhaustive proof from 32 bits to longer FP representations for a 
particular implementation, a problem that I believe to be wholly 
unlike the simple examples that you later provided (those all 
enjoyed very clear domain co-domain mappings while suspected 
opacity of that mapping is the main concern regarding your "no 
problem" assertion).

Also, please understand that I do not regard your time as more 
valuable than the time of your readers.  In that spirit I suggest 
that direct answers to questions regarding simple topics ("no 
problem" topics), are preferable to assertions that you don't 
have time to help others understand.  Also note that "I was 
mistaken" and "I'm not sure what you mean, could you clarify 
x,y,z?" are perfectly acceptable responses (that I've used on 
more than one occasion and will, no doubt, use again in the 
future).
Jan 27 2021
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Wednesday, 27 January 2021 at 09:09:08 UTC, Bruce Carneal 
wrote:

 No, you made an assertion regarding the tractable extension of 
 an exhaustive proof from 32 bits to longer FP representations 
 for a particular implementation, a problem that I believe to be 
 wholly unlike the simple examples


The original statement was that there was only a choice between 
exhaustive testing and a full formal proof. Then there was 
confusion between proving the correctness of tables, algorithms 
and the actual implementation.

Nobody wants to implement an algorithm for which there are no 
proofs of correctness. That is the basic foundation we have to 
presume, so a proof of the  abstract algorithm is not wasted even 
if you only test the implementation. That proof is kinda part of 
the specification you base your implementation and testing on.

When you implement the algorithm you also have to consider how it 
will be tested (including partial proofs). The "no problem" as 
related to not having to choose between an exhaustive proof and 
full formal verification. Neither option is likely in the D 
community.

I pointed out that one can test the boundary cases. I have 
clearly not studied the details of the implementation. It was a 
general suggestion for when neither a full formal proof is likely 
or exhaustive testing is reasonable.



 valuable than the time of your readers.  In that spirit I 
 suggest that direct answers to questions regarding simple 
 topics ("no problem" topics), are preferable to assertions that 
 you don't have time to help others understand.


I haven't made any such assertion. If you ask questions, I'll 
answer them to my ability. Please stop making assumptions.

We are talking about finite input, finite input, small scale, and 
fairly regular. Clearly not intractable.
Jan 27 2021
parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Wednesday, 27 January 2021 at 09:37:34 UTC, Ola Fosheim 
Grøstad wrote:

 On Wednesday, 27 January 2021 at 09:09:08 UTC, Bruce Carneal 
 wrote:

 I haven't made any such assertion. If you ask questions, I'll 
 answer them to my ability. Please stop making assumptions.


Great.  Two questions: 1) Do you believe that a trivial 
domain/co-domain mapping, like those in the examples you gave, 
exists for the problem under discussion? and 2) If so, do you 
have time to provide a proof?
Jan 27 2021
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Wednesday, 27 January 2021 at 17:00:36 UTC, Bruce Carneal 
wrote:

 Great.  Two questions: 1) Do you believe that a trivial 
 domain/co-domain mapping, like those in the examples you gave, 
 exists for the problem under discussion? and


Certainly trivial from a theoretical perspective, in the sense 
that they are finite and therefore can be easily tabulated. If 
you want a more compact form you probably should look at modular 
arithmetics. You left out an important criterion, space-time 
efficiency.

The inverse mapping is also not terribly complex, but first you 
need to establish what you want to show. In the context of 
Phobos, minimal length is of little importance, it has not impact 
on correct usage. We don't have to care if the algorithm produces 
more digits than necessary, so we can limit ourselves to the 
inverse mapping from decimal to binary. Basically proving that we 
then get the x = f⁻¹(f(x)) = id(x).



 2) If so, do you have time to provide a proof?


Proof of what? And are you willing to pay for it?

(I suggest you drop the juvenile tone, it is annoying.)
Jan 27 2021
parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Wednesday, 27 January 2021 at 22:49:11 UTC, Ola Fosheim 
Grøstad wrote:

 On Wednesday, 27 January 2021 at 17:00:36 UTC, Bruce Carneal 
 wrote:

 Great.  Two questions: 1) Do you believe that a trivial 
 domain/co-domain mapping, like those in the examples you gave, 
 exists for the problem under discussion? and


 Certainly trivial from a theoretical perspective, in the sense 
 that they are finite and therefore can be easily tabulated. If 
 you want a more compact form you probably should look at 
 modular arithmetics. You left out an important criterion, 
 space-time efficiency.

 The inverse mapping is also not terribly complex, but first you 
 need to establish what you want to show. In the context of 
 Phobos, minimal length is of little importance, it has not 
 impact on correct usage. We don't have to care if the algorithm 
 produces more digits than necessary, so we can limit ourselves 
 to the inverse mapping from decimal to binary. Basically 
 proving that we then get the x = f⁻¹(f(x)) = id(x).



 2) If so, do you have time to provide a proof?


 Proof of what? And are you willing to pay for it?

 (I suggest you drop the juvenile tone, it is annoying.


Perhaps you mistook my meaning when I used the term "trivial".  I 
could also have used "simple", "readily understood", "clearly 
provable", etc.

Regardless, you clearly do not understand what I'm asking in 
question 1) and I do not think it likely that additional 
interaction on this topic will be useful to either of us.
Jan 27 2021
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Thursday, 28 January 2021 at 02:25:57 UTC, Bruce Carneal wrote:

 Regardless, you clearly do not understand what I'm asking in 
 question 1) and I do not think it likely that additional 
 interaction on this topic will be useful to either of us.


Asking for a mapping does not really make much sense without 
specifying the domain/codomain, but my answer actually holds even 
then.

Anyway, if you _actually_ are interested in this topic then you 
could start by looking at automatic test case generation using 
SMT solvers.
Jan 28 2021
next sibling parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Thursday, 28 January 2021 at 08:30:40 UTC, Ola Fosheim Grøstad 
wrote:

 On Thursday, 28 January 2021 at 02:25:57 UTC, Bruce Carneal 
 wrote:

 Regardless, you clearly do not understand what I'm asking in 
 question 1) and I do not think it likely that additional 
 interaction on this topic will be useful to either of us.


 Asking for a mapping does not really make much sense without 
 specifying the domain/codomain, but my answer actually holds 
 even then.


For the problem under discussion the domain is 0 .. 2**NBits 
(binary FP) and the codomain is the problem specified string 
output of the function.  This has not changed and I had thought 
it was clear to all concerned throughout.

The correctness check for the mapping in this case is trivial, by 
which I mean: obvious, readily understood, not needing further 
explanation, ... a *good* thing in this context.


 Anyway, if you _actually_ are interested in this topic then you 
 could start by looking at automatic test case generation using 
 SMT solvers.


I am actually interested in proving correctness by establishing 
full coverage of the domain with something less expensive than 
direct enumeration, less expensive than a for loop across all 
possibilities (an SMT-like solution).  This is what I thought 
that you said you had accomplished with a trivial coverage, your 
"no problem" remark.  IOW, I thought you claimed to have solved 
the problem.

I found such a claim remarkable, I did not see it, so I sought 
clarification.  IIUC now, I was mistaken then.  You have no 
particular insight to offer toward the solution of the above 
problem and, by your lights, never made such a claim.

Apparently I took your well meaning remarks much too seriously.
Jan 28 2021
next sibling parent Bruce Carneal <bcarneal gmail.com> writes:
On Thursday, 28 January 2021 at 15:13:57 UTC, Bruce Carneal wrote:

 On Thursday, 28 January 2021 at 08:30:40 UTC, Ola Fosheim 
 Grøstad wrote:

 For the problem under discussion the domain is 0 .. 2**NBits 
 (binary FP)...


That should be 2**N - 1.
Jan 28 2021
prev sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Thursday, 28 January 2021 at 15:13:57 UTC, Bruce Carneal wrote:

 For the problem under discussion the domain is 0 .. 2**NBits 
 (binary FP) and the codomain is the problem specified string 
 output of the function.  This has not changed and I had thought 
 it was clear to all concerned throughout.


Let's backtrack then. My suggestion was that one does an informal 
proof of the easier aspects one can reason about and then do 
testing to cover those aspects which one cannot convince oneself 
of. So in order to list those tests one would have to do a deep 
analysis of the actual implementation informed by the 
properties/proofs of the abstract algorithm (the spec). Without 
such an analysis one cannot give examples of dependencies 
expressed as propositions.

The core problem float2string is comparable to fixedpoint2string 
which is comparable to integer2string, because the transform from 
float to fixed point is trivial. (We also note that float is 
base2 and the target is base10, and that 10=5·2 so we may be 
rewarded for paying attention to modulo 5.) Then we may choose to 
represent a base 10 digit with something that is easier to deal 
with for a solver. We then need to think about, not increments of 
1, but relationships in terms of modular arithmetic/congruence - 
related formalizations.



 I am actually interested in proving correctness by establishing 
 full coverage of the domain with something less expensive than 
 direct enumeration, less expensive than a for loop across all 
 possibilities (an SMT-like solution).


SMT/SAT based solutions are not like a for-loop across all 
possibilities.

Are you actually serious about proving correctness? I don't get 
that feeling.



 You have no particular insight to offer toward the solution of 
 the above problem and, by your lights, never made such a claim.


I am not sure what you mean by this, but you sure manage to make 
it sound offensive... I've suggested utilizing bit-blasting, 
identity transform, modular arithmetics etc. I've never hinted or 
suggested that I have any intent of working on this problem, and 
explicitly stated that I have not taken a close look at the Mir 
implementation, nor do I intend to.

I do however refute the idea that an exhaustive test is needed, 
since the problem involves regular patterns.
Jan 28 2021
next sibling parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Thursday, 28 January 2021 at 23:27:28 UTC, Ola Fosheim Grøstad 
wrote:

 On Thursday, 28 January 2021 at 15:13:57 UTC, Bruce Carneal 
 wrote:

 For the problem under discussion the domain is 0 .. 2**NBits 
 (binary FP) and the codomain is the problem specified string 
 output of the function.  This has not changed and I had 
 thought it was clear to all concerned throughout.


 Let's backtrack then. My suggestion was that one does an 
 informal proof of the easier aspects one can reason about and 
 then do testing to cover those aspects which one cannot 
 convince oneself of. So in order to list those tests one would 
 have to do a deep analysis of the actual implementation 
 informed by the properties/proofs of the abstract algorithm 
 (the spec). Without such an analysis one cannot give examples 
 of dependencies expressed as propositions.

 The core problem float2string is comparable to 
 fixedpoint2string which is comparable to integer2string, 
 because the transform from float to fixed point is trivial. (We 
 also note that float is base2 and the target is base10, and 
 that 10=5·2 so we may be rewarded for paying attention to 
 modulo 5.) Then we may choose to represent a base 10 digit with 
 something that is easier to deal with for a solver. We then 
 need to think about, not increments of 1, but relationships in 
 terms of modular arithmetic/congruence - related formalizations.



 I am actually interested in proving correctness by 
 establishing full coverage of the domain with something less 
 expensive than direct enumeration, less expensive than a for 
 loop across all possibilities (an SMT-like solution).


 SMT/SAT based solutions are not like a for-loop across all 
 possibilities.


No, of course not.  The parenthetical phrase was meant to apply 
to everything that preceeded it.  An SMT like solution is what I 
thought you had asserted, something that substantially cut down 
the work while provably covering the full domain.


 Are you actually serious about proving correctness? I don't get 
 that feeling.



 You have no particular insight to offer toward the solution of 
 the above problem and, by your lights, never made such a claim.


 I am not sure what you mean by this, but you sure manage to 
 make it sound offensive... I've suggested utilizing 
 bit-blasting, identity transform, modular arithmetics etc. I've 
 never hinted or suggested that I have any intent of working on 
 this problem, and explicitly stated that I have not taken a 
 close look at the Mir implementation, nor do I intend to.

 I do however refute the idea that an exhaustive test is needed, 
 since the problem involves regular patterns.


Well, you've not refuted anything that I can see.  You've 
asserted something, yes, something that I think is quite useful 
if provable.  The intutition that prompts you to make such an 
assertion is what I'm most interested in.  I do not believe the 
assertion is provable but would be very happy to be proven wrong 
as that would be a win for everyone.

Since you continue to take offense at my writing, where none was 
intended, I think direct two way communication would be better 
than continuing here.  I'll be hanging out at beerconf if you 
think it's worth your time to converge on understanding.  Even if 
we aren't able to take your intuition to a proof or refutation 
quickly, we should at least be able to comprehend a lack of ill 
will.
Jan 28 2021
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 29 January 2021 at 02:58:38 UTC, Bruce Carneal wrote:

 The parenthetical phrase was meant to apply to everything that 
 preceeded it.  An SMT like solution is what I thought you had 
 asserted, something that substantially cut down the work while 
 provably covering the full domain.


I am not asserting anything, other than that I don't think full 
formal verification (unless bitblasting works) is within the 
perimeter of the D community, so that leaves informal proofs 
combined with selective testing as the viable option that the D 
community as a whole (not any specific individual) can accomplish.

A solver is a tool that can be used to make this viable. Without 
a solver, maybe a reimplementation with a correspondence proof is 
easier.



 better than continuing here.  I'll be hanging out at beerconf 
 if you think it's worth your time to converge on understanding.



I like the idea of beerconf, but I have a deliverable deadline on 
monday, so I don't have time this week.
Jan 29 2021
parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Friday, 29 January 2021 at 13:42:49 UTC, Ola Fosheim Grøstad 
wrote:

 On Friday, 29 January 2021 at 02:58:38 UTC, Bruce Carneal wrote:

 The parenthetical phrase was meant to apply to everything that 
 preceeded it.  An SMT like solution is what I thought you had 
 asserted, something that substantially cut down the work while 
 provably covering the full domain.


 I am not asserting anything, other than that I don't think full 
 formal verification (unless bitblasting works) is within the 
 perimeter of the D community, so that leaves informal proofs 
 combined with selective testing as the viable option that the D 
 community as a whole (not any specific individual) can 
 accomplish.


Then I misunderstood you all along.  I thought that you were 
describing something that would be part of a formal proof.

As an aside: I consider an exhaustive f32 proof to be very strong 
evidence that an implementation will likely be correct for larger 
formats.


 A solver is a tool that can be used to make this viable. 
 Without a solver, maybe a reimplementation with a 
 correspondence proof is easier.



 better than continuing here.  I'll be hanging out at beerconf 
 if you think it's worth your time to converge on understanding.



 I like the idea of beerconf, but I have a deliverable deadline 
 on monday, so I don't have time this week.


OK.  I hope we have the opportunity to chat directly at a later 
date.  Good luck meeting your deadline.
Jan 29 2021
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 29 January 2021 at 14:24:17 UTC, Bruce Carneal wrote:

 Then I misunderstood you all along.  I thought that you were 
 describing something that would be part of a formal proof.


A formal proof would have to be machine checked. So you need a 
good solver/verifiers. And experience to make good use of, and 
patience... I think we can safely say that this is out of scope 
for the D community at this point.
Jan 29 2021
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 29 January 2021 at 18:35:54 UTC, Ola Fosheim Grøstad 
wrote:

 On Friday, 29 January 2021 at 14:24:17 UTC, Bruce Carneal wrote:

 Then I misunderstood you all along.  I thought that you were 
 describing something that would be part of a formal proof.


 A formal proof would have to be machine checked. So you need a 
 good solver/verifiers. And experience to make good use of, and 
 patience... I think we can safely say that this is out of scope 
 for the D community at this point.


And you would also need to annotate the D code with Hoare logic 
and generate verification conditions. Although there are tools 
that can help with that. But you would still need expertise to 
make good use of it. It is not a push-button topic.

The only other alternative would be bit blasting, as I mentioned, 
which may or may not work out. Probably not if the code is too 
convoluted, but it might. Depends on the solver and structure of 
the input.
Jan 29 2021
parent reply sarn <sarn theartofmachinery.com> writes:
On Friday, 29 January 2021 at 18:48:42 UTC, Ola Fosheim Grøstad 
wrote:

 And you would also need to annotate the D code with Hoare logic 
 and generate verification conditions. Although there are tools 
 that can help with that. But you would still need expertise to 
 make good use of it. It is not a push-button topic.

 The only other alternative would be bit blasting, as I 
 mentioned, which may or may not work out. Probably not if the 
 code is too convoluted, but it might. Depends on the solver and 
 structure of the input.


Have you seen KLEE?  It applies a solver like Z3 to normal code 
with assert() statements, as long as it can be compiled to LLVM 
bitcode and run with KLEE-compatible standard libraries.

The original KLEE doesn't support floating point, but there's a 
fork that does (which I've never used).

https://theartofmachinery.com/2019/05/28/d_and_klee.html
(There are some things I need to fix/update in that post.)
Jan 29 2021
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 29 January 2021 at 21:11:02 UTC, sarn wrote:

 Have you seen KLEE?  It applies a solver like Z3 to normal code 
 with assert() statements, as long as it can be compiled to LLVM 
 bitcode and run with KLEE-compatible standard libraries.


I've only read about KLEE, which looks interesting. Using LLVMIR  
is one approach one can use for analysis when the input/output is 
tiny. You can (after unrolling) convert the IR  to  64 logical 
propositions. One big logical (boolean) formula for each bit in 
the output.

In this specific application you could try to prove that output 
bit 1 only depends on input bit 1, output bit 2 only depends on 
input bit 2 and so on.

(After applying the inverse function, so that the function 
returns the same value as the input.)
Jan 29 2021
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 29 January 2021 at 22:03:26 UTC, Ola Fosheim Grøstad 
wrote:

 input/output is tiny. You can (after unrolling) convert the IR  
 to  64 logical propositions. One big logical (boolean) formula 
 for each bit in the output.


Or more likely 128 boolean expressions, since you probably have 
more chance of resolution if you first show that there is no 
solution for output1 == false && input1 == true, then you do the 
same for output1 == true && input1 == false.
Jan 30 2021
prev sibling parent reply Afgdr <zerzre.rertert gmx.com> writes:
On Thursday, 28 January 2021 at 23:27:28 UTC, Ola Fosheim Grøstad 
wrote:

 I do however refute the idea that an exhaustive test is needed, 
 since the problem involves regular patterns.


how about a full coverage of a half float type, assuming the 
function tested works the same with float and double and anay 
arbitrary lond FP type, e.g template param for mantissa and exp. 
Sof if a smaller FP type fully passes the for loop test, e.g all 
permutations we can assume bigger FP types will be 100% correctly 
converted.
Jan 30 2021
parent reply Afgdr <zerzre.rertert gmx.com> writes:
On Saturday, 30 January 2021 at 11:02:54 UTC, Afgdr wrote:

 On Thursday, 28 January 2021 at 23:27:28 UTC, Ola Fosheim 
 Grøstad wrote:

 I do however refute the idea that an exhaustive test is 
 needed, since the problem involves regular patterns.


 how about a full coverage of a half float type, assuming the 
 function tested works the same with float and double and anay 
 arbitrary lond FP type, e.g template param for mantissa and 
 exp. Sof if a smaller FP type fully passes the for loop test, 
 e.g all permutations we can assume bigger FP types will be 100% 
 correctly converted.


Well I forgot that it may use LUTs so maybe not in this case, but 
otherwise you should get the idea.
Jan 30 2021
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Saturday, 30 January 2021 at 11:06:34 UTC, Afgdr wrote:

 Well I forgot that it may use LUTs so maybe not in this case, 
 but otherwise you should get the idea.


Yes, I get your idea, but I think one has to be a bit more 
careful and base what is tested on what the implementation does. 
For instance, float32 does not expose overflow issues.

We can assume that LUTs are correct if they are pre-generated, 
though.
Jan 30 2021
prev sibling parent Bruce Carneal <bcarneal gmail.com> writes:
On Thursday, 28 January 2021 at 08:30:40 UTC, Ola Fosheim Grøstad 
wrote:

 On Thursday, 28 January 2021 at 02:25:57 UTC, Bruce Carneal 
 wrote:

 Regardless, you clearly do not understand what I'm asking in 
 question 1) and I do not think it likely that additional 
 interaction on this topic will be useful to either of us.


 Asking for a mapping does not really make much sense without 
 specifying the domain/codomain, but my answer actually holds 
 even then.

 Anyway, if you _actually_ are interested in this topic then you 
 could start by looking at automatic test case generation using 
 SMT solvers.


We seem to repeatedly misunderstand one another on this topic so 
a quick back and forth, without burdening others in the forum, 
would be a good way to go from here.

I'll be at the end-of-Jan beerconf for much of the time (I'm 
GMT+8 but will probably overlap with your daytime hours) so if 
you're interested we can establish a 2-way comm channel there and 
quickly, I believe, converge on understanding.
Jan 28 2021
prev sibling parent reply Bruce Carneal <bcarneal gmail.com> writes:
On Tuesday, 26 January 2021 at 20:27:25 UTC, Ola Fosheim Grøstad 
wrote:

 On Tuesday, 26 January 2021 at 19:02:53 UTC, Bruce Carneal 
 wrote:

 If you can construct a tractable exhaustive proof of an 
 implementation, which is what I believe you asserted in this 
 case, then you don't need any other proof.


 Of course you do, you need proof of the tests being correct...


I believed that to be obvious.  There is no utility in 
exhaustively looping over tests that are incorrect.  The domain 
<==> co-domain properties in this case means that the correctness 
check is direct.


 can be skipped is tantamount to saying that you know the 
 implementation performs correctly in those regions.


 In general, if one understands the algorithm as implemented 
 then one can either manually or automatically prove certain 
 regions/ranges. Then you only need to test the regions/ranges 
 that are hard to prove.

 For instance, for a converter from int to string, the most 
 likely failure point will be tied to crossing between "9" and 
 "0" as well as the ends of the base-2 input. Meaning, if it 
 works for 1,2,3, you know that it also works for 4,5,6,7,8, but 
 maybe not 9,10.


Yes.  So now we have to prove that we can subset the exhaustive 
test.

This is something like the algorithm development technique that 
starts with a backtracking solution (full enumeration) and then 
prunes away via memoization or other to achieve a lower 
complexity.  If, OTOH, I start in the middle, asserting that I 
"know" what the shape of the problem is, then I'm on shaky ground.

As practicing programmers we live with "shaky ground" every day, 
but I'm hoping we can do better in this case.  It's already 
moving in a good direction.
Jan 26 2021
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 26 January 2021 at 20:45:22 UTC, Bruce Carneal wrote:

 As practicing programmers we live with "shaky ground" every 
 day, but I'm hoping we can do better in this case.  It's 
 already moving in a good direction.


Yes, the real issue in practice is constantly changing 
requirements and evolving software over time.

We don't really have programming languages that support 
restructuring/modifying code very well. And well, if you have 
lots of "correct" tests, it becomes even more expensive to 
change...

So, breaking things up into smaller units with concepts like 
actors might be a way to go, perhaps. Dunno.
Jan 26 2021