Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
On Sep 13, 2013, at 7:02 PM, Dmitry Nadezhin wrote: I agree with 1100 for this review (JDK7). OK. I will post an approval request to 7u-dev for the patch as-is. I think that we shouldn't change from 1100 to 768 in JDK8 because this is a small performance enhancement. This will save time for fixing other bugs. Fine with me. The performance enhancement could be smarter if we replace constant MAX_NDIGIT by some piece-linear function function maxNDigit(decExponent). See: http://cr.openjdk.java.net/~bpb/nDigits/java/double.pdf I'd like to postpone this to JDK9 . Thanks, Brian
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
I would suggest leaving it at 1100 for this review (JDK7) and to 768 (0x003) in JDK8. The latter will require another issue to be filed. On Sep 12, 2013, at 9:25 PM, Dmitry Nadezhin wrote: For me, it is the only consideration. I'm sure in 768 because I proved it formally using ACL2 tool. On Fri, Sep 13, 2013 at 7:45 AM, David M. Lloyd david.ll...@redhat.comwrote: If that's the only consideration then just use 0x300 instead, which is easier to read *and* makes more sense anyway, in the context of the test. On 09/12/2013 10:13 PM, Dmitry Nadezhin wrote: Should we change conservative constant 1100 to optimal constant 768 ? My opinion is no (in JDK7), because the constant 1100 has lower cost of review. I mean that chances that a reviewer approves 1100 are higher than chances that [s]he approves 768.
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
I agree with 1100 for this review (JDK7). I think that we shouldn't change from 1100 to 768 in JDK8 because this is a small performance enhancement. This will save time for fixing other bugs. The performance enhancement could be smarter if we replace constant MAX_NDIGIT by some piece-linear function function maxNDigit(decExponent). See: http://cr.openjdk.java.net/~bpb/nDigits/java/double.pdf I'd like to postpone this to JDK9 . On Sat, Sep 14, 2013 at 4:39 AM, Brian Burkhalter brian.burkhal...@oracle.com wrote: I would suggest leaving it at 1100 for this review (JDK7) and to 768 (0x003) in JDK8. The latter will require another issue to be filed. On Sep 12, 2013, at 9:25 PM, Dmitry Nadezhin wrote: For me, it is the only consideration. I'm sure in 768 because I proved it formally using ACL2 tool. On Fri, Sep 13, 2013 at 7:45 AM, David M. Lloyd david.ll...@redhat.com wrote: If that's the only consideration then just use 0x300 instead, which is easier to read *and* makes more sense anyway, in the context of the test. On 09/12/2013 10:13 PM, Dmitry Nadezhin wrote: Should we change conservative constant 1100 to optimal constant 768 ? My opinion is no (in JDK7), because the constant 1100 has lower cost of review. I mean that chances that a reviewer approves 1100 are higher than chances that [s]he approves 768.
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
This explanation seems to combine numbers of binary digits (1075) and numbers of decimal digits (17), and therefore makes me a little nervous, though I think 1100 is a conservative choice that, even if not 100% correct, will be 99.(over 700 9s)% correct. David On 2013-09-12, at 1:17 AM, Dmitry Nadezhin dmitry.nadez...@gmail.com wrote: When I prepared the patch I didn't try to find the optimal MAX_NDIGITS, but I was sure that MAX_NDIGITS = 1100 is enough. Here is an expanation: 1) If value of decimal string is larger than pow(10,309) then it is converted to positive infinity before the test of nDigits; 2) If value of decimal string is smaller than pow(10,309) and larger than pow(2,53) then it rounds to Java double with ulp = 2. Half-ulp = 1. The patch is correct when decimal ULP of kept digits is 1 or less. It is true beacuse MAX_NDIGITS = 1100 309; 3) If value of decimal string is smaller than pow(2,53) but larger than 0.5*Doulle.MIN_VALUE = pow(2,-1022-52-1), than binary ULP is a multiple of pow(2,-1074). Half-ULP is a multiple of pow(2,-1075). The patch is correct when decimal ULP of kept digits is pow(10,-1075) of less. pow(2,53) has 17 decimal decimal digits. MAX_NDIGITS = 1100 1075 + 17 . 4) If value of decimal string is smaller than 0.5*Double.MIN_VALUE then it is converted to zero before the test of nDigits. You can treat replacement of 1075 + 17 by 1100 as my paranoia. It still was interesting for me what is the optimal truncation of decimal string.
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
The reason while binary and decimal digits are mixed can be ullustrated by such example. It is necessary 3 decimal fraction digits to represent exactly pbinary power pow(2,-3) : pow(2,-3)=1/8=0.125 On Thu, Sep 12, 2013 at 3:57 PM, David Chase david.r.ch...@oracle.comwrote: This explanation seems to combine numbers of binary digits (1075) and numbers of decimal digits (17), and therefore makes me a little nervous, though I think 1100 is a conservative choice that, even if not 100% correct, will be 99.(over 700 9s)% correct. David On 2013-09-12, at 1:17 AM, Dmitry Nadezhin dmitry.nadez...@gmail.com wrote: When I prepared the patch I didn't try to find the optimal MAX_NDIGITS, but I was sure that MAX_NDIGITS = 1100 is enough. Here is an expanation: 1) If value of decimal string is larger than pow(10,309) then it is converted to positive infinity before the test of nDigits; 2) If value of decimal string is smaller than pow(10,309) and larger than pow(2,53) then it rounds to Java double with ulp = 2. Half-ulp = 1. The patch is correct when decimal ULP of kept digits is 1 or less. It is true beacuse MAX_NDIGITS = 1100 309; 3) If value of decimal string is smaller than pow(2,53) but larger than 0.5*Doulle.MIN_VALUE = pow(2,-1022-52-1), than binary ULP is a multiple of pow(2,-1074). Half-ULP is a multiple of pow(2,-1075). The patch is correct when decimal ULP of kept digits is pow(10,-1075) of less. pow(2,53) has 17 decimal decimal digits. MAX_NDIGITS = 1100 1075 + 17 . 4) If value of decimal string is smaller than 0.5*Double.MIN_VALUE then it is converted to zero before the test of nDigits. You can treat replacement of 1075 + 17 by 1100 as my paranoia. It still was interesting for me what is the optimal truncation of decimal string.
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
On 09/12/2013 09:17 AM, Dmitry Nadezhin wrote: The patch is correct when decimal ULP of kept digits is pow(10,-1075) of less. pow(2,53) has 17 decimal decimal digits. MAX_NDIGITS = 1100 1075 + 17 . OK. That makes more sense. Can we please add the short comment in the code (maybe next time around)? I expected to see something like The value below is chosen as the conservative threshold. We can demonstrate (link) that decimal ulp should be less than 10^(-1075) to guarantee correctness; we also compensate for binary mantissa which takes 53 binary digits, or 17 decimal ones. Hence, 1075+17 =~ 1100. -Aleksey.
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
On 2013-09-12, at 8:18 AM, Dmitry Nadezhin dmitry.nadez...@gmail.com wrote: The reason while binary and decimal digits are mixed can be ullustrated by such example. It is necessary 3 decimal fraction digits to represent exactly pbinary power pow(2,-3) : pow(2,-3)=1/8=0.125 On Thu, Sep 12, 2013 at 3:57 PM, David Chase david.r.ch...@oracle.comwrote: This explanation seems to combine numbers of binary digits (1075) and numbers of decimal digits (17), and therefore makes me a little nervous, though I think 1100 is a conservative choice that, even if not 100% correct, will be 99.(over 700 9s)% correct. David Yes, but you are adding them. It is as if you took two lengths, 1075 feet and 17 yards, added them, rounded up, and said that 1100 yards will be adequate (which is entirely true, though perhaps overconservative). Overconservative is okay. 2^-1075 is the binary ulp, give or take a fencepost, not the decimal ulp. David
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
I think the reason you use 1075 digits is because it takes 1075 decimal digits behind the decimal point to exactly represent 2^-1075, and that is 1/2 ulp. When you discard the tail, if it happens to be all zeroes, I hope you replace it with a zero, not a one, because otherwise you can round incorrectly if the answer is otherwise equal to EVEN + 1/2 ULP. EVEN + 1/2 ULP rounds to EVEN, EVEN + 1/2 ULP + 1 rounds to EVEN + 1. Whoops, no, you don't do that. But I'd call that another bug, and not one worth getting terribly excited about. Strictly speaking, if your input is decimal_rep_of_half_ulp + a billion zeroes + 1, then the answer is 1 ulp (2^-1074), if the trailing one is missing, then the answer is zero (which is even in the mantissa). David On 2013-09-12, at 10:37 AM, David Chase david.r.ch...@oracle.com wrote: On 2013-09-12, at 8:18 AM, Dmitry Nadezhin dmitry.nadez...@gmail.com wrote: The reason while binary and decimal digits are mixed can be ullustrated by such example. It is necessary 3 decimal fraction digits to represent exactly pbinary power pow(2,-3) : pow(2,-3)=1/8=0.125 On Thu, Sep 12, 2013 at 3:57 PM, David Chase david.r.ch...@oracle.comwrote: This explanation seems to combine numbers of binary digits (1075) and numbers of decimal digits (17), and therefore makes me a little nervous, though I think 1100 is a conservative choice that, even if not 100% correct, will be 99.(over 700 9s)% correct. David Yes, but you are adding them. It is as if you took two lengths, 1075 feet and 17 yards, added them, rounded up, and said that 1100 yards will be adequate (which is entirely true, though perhaps overconservative). Overconservative is okay. 2^-1075 is the binary ulp, give or take a fencepost, not the decimal ulp. David
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
Never mind, this is in the context of FloatingDecimal and any trailing zeroes are properly discarded. Carry on, this code looks correct, despite my misunderstanding the explanation. David On 2013-09-12, at 12:32 PM, David Chase david.r.ch...@oracle.com wrote: I think the reason you use 1075 digits is because it takes 1075 decimal digits behind the decimal point to exactly represent 2^-1075, and that is 1/2 ulp. When you discard the tail, if it happens to be all zeroes, I hope you replace it with a zero, not a one, because otherwise you can round incorrectly if the answer is otherwise equal to EVEN + 1/2 ULP. EVEN + 1/2 ULP rounds to EVEN, EVEN + 1/2 ULP + 1 rounds to EVEN + 1. Whoops, no, you don't do that. But I'd call that another bug, and not one worth getting terribly excited about. Strictly speaking, if your input is decimal_rep_of_half_ulp + a billion zeroes + 1, then the answer is 1 ulp (2^-1074), if the trailing one is missing, then the answer is zero (which is even in the mantissa). David On 2013-09-12, at 10:37 AM, David Chase david.r.ch...@oracle.com wrote: On 2013-09-12, at 8:18 AM, Dmitry Nadezhin dmitry.nadez...@gmail.com wrote: The reason while binary and decimal digits are mixed can be ullustrated by such example. It is necessary 3 decimal fraction digits to represent exactly pbinary power pow(2,-3) : pow(2,-3)=1/8=0.125 On Thu, Sep 12, 2013 at 3:57 PM, David Chase david.r.ch...@oracle.comwrote: This explanation seems to combine numbers of binary digits (1075) and numbers of decimal digits (17), and therefore makes me a little nervous, though I think 1100 is a conservative choice that, even if not 100% correct, will be 99.(over 700 9s)% correct. David Yes, but you are adding them. It is as if you took two lengths, 1075 feet and 17 yards, added them, rounded up, and said that 1100 yards will be adequate (which is entirely true, though perhaps overconservative). Overconservative is okay. 2^-1075 is the binary ulp, give or take a fencepost, not the decimal ulp. David
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
Aleksey, I like your wording of the comment. Thank you very much. I would reformulate a little: We can demonstrate (link) that decimal ulp should be less than 10^(-1075) to guarantee correctness === We can demonstrate (link) that decimal ulp less than 10^(-1075) is enough to guarantee correctness. because decimal ulp may be larger than 10^(-1075) for some inputs. For example, for decimal string 1. binary half-ulp is 2^(-53) and decimal ulp 10^(-53) is enough . On Thu, Sep 12, 2013 at 6:32 PM, Aleksey Shipilev aleksey.shipi...@oracle.com wrote: On 09/12/2013 09:17 AM, Dmitry Nadezhin wrote: The patch is correct when decimal ULP of kept digits is pow(10,-1075) of less. pow(2,53) has 17 decimal decimal digits. MAX_NDIGITS = 1100 1075 + 17 . OK. That makes more sense. Can we please add the short comment in the code (maybe next time around)? I expected to see something like The value below is chosen as the conservative threshold. We can demonstrate (link) that decimal ulp should be less than 10^(-1075) to guarantee correctness; we also compensate for binary mantissa which takes 53 binary digits, or 17 decimal ones. Hence, 1075+17 =~ 1100. -Aleksey.
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
JDK repository constains sources and tests now. Where should proofs live ? And also where should benchmarks live ? On Thu, Sep 12, 2013 at 10:32 PM, Brian Burkhalter brian.burkhal...@oracle.com wrote: What should be put in for link? Thanks, Brian On Sep 12, 2013, at 11:10 AM, Dmitry Nadezhin wrote: Aleksey, I like your wording of the comment. Thank you very much. I would reformulate a little: We can demonstrate (link) that decimal ulp should be less than 10^(-1075) to guarantee correctness === We can demonstrate (link) that decimal ulp less than 10^(-1075) is enough to guarantee correctness. because decimal ulp may be larger than 10^(-1075) for some inputs. For example, for decimal string 1. binary half-ulp is 2^(-53) and decimal ulp 10^(-53) is enough .
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
What should be put in for link? Thanks, Brian On Sep 12, 2013, at 11:10 AM, Dmitry Nadezhin wrote: Aleksey, I like your wording of the comment. Thank you very much. I would reformulate a little: We can demonstrate (link) that decimal ulp should be less than 10^(-1075) to guarantee correctness === We can demonstrate (link) that decimal ulp less than 10^(-1075) is enough to guarantee correctness. because decimal ulp may be larger than 10^(-1075) for some inputs. For example, for decimal string 1. binary half-ulp is 2^(-53) and decimal ulp 10^(-53) is enough .
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
On 2013-09-12, at 1:17 AM, Dmitry Nadezhin dmitry.nadez...@gmail.com wrote: The optimal constant for double conversion could be 768 , the optimal constant for float conversion could be 142, but I leave this optimization to JDK 9. It would be helpful to mention in the proof/comment, that 768 refers to the decimal representation that has had leading zeroes between decimal point and mantissa trimmed. An exact case is the decimal representation of the sum of 2^-1022 + 2^-1075 This has a decimal point, then 307 zeroes, non-zeroes at 308 (2) and 1075 (5) (and usually non-zeroes between) for a span of 768 decimal digits between the leading and trailing zeroes. (There are other screw cases. Here, 2^-1022 is the minimum normalized-rep double, and 2^-1075 is 1/2 ulp for doubles with binary exponent -1022, which is represented as 1 in IEEE format.) Appending any trailing non-zero on this decimal representation rounds up; nothing trailing rounds down. If the final digit 5 is instead a 6, it always rounds up, if it is a 4 it always rounds down no matter what is appended. There are other screw cases, but they always involve 2^-1075 because that requires the maximum number of decimal digits for its representation. David
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
I know, I checked the census. The Reviewed-by header field can include any OpenJDK member AFAIK. The approval for pushing is a separate story and has to be handled via e-mail on the 7u-dev list (and a 7u-dev committer will be needed eventually). Thanks, Brian On Sep 12, 2013, at 1:57 PM, David Chase wrote: Careful, I don't think I'm a Reviewer. I merely had the misfortune to care a whole lot about this stuff once long long ago.
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
On Sep 12, 2013, at 1:00 PM, David Chase wrote: On 2013-09-12, at 1:17 AM, Dmitry Nadezhin dmitry.nadez...@gmail.com wrote: The optimal constant for double conversion could be 768 , the optimal constant for float conversion could be 142, but I leave this optimization to JDK 9. It would be helpful to mention in the proof/comment, that 768 refers to the decimal representation that has had leading zeroes between decimal point and mantissa trimmed. I updated the webrev to include a comment for MAX_NDIGITS sans both hyperlink and the foregoing verbiage: http://cr.openjdk.java.net/~bpb/8024356/ If there is any more tweaking of comments which needs to be effected prior to an approval request being posted to 7u-dev, please let me know. Thanks, Brian
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
On 13.09.2013, at 0:49, Brian Burkhalter brian.burkhal...@oracle.com wrote: I updated the webrev to include a comment for MAX_NDIGITS sans both hyperlink and the foregoing verbiage: http://cr.openjdk.java.net/~bpb/8024356/ Thumbs up. -Aleksey
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
Careful, I don't think I'm a Reviewer. I merely had the misfortune to care a whole lot about this stuff once long long ago. David On 2013-09-12, at 4:49 PM, Brian Burkhalter brian.burkhal...@oracle.com wrote: On Sep 12, 2013, at 1:00 PM, David Chase wrote: On 2013-09-12, at 1:17 AM, Dmitry Nadezhin dmitry.nadez...@gmail.com wrote: The optimal constant for double conversion could be 768 , the optimal constant for float conversion could be 142, but I leave this optimization to JDK 9. It would be helpful to mention in the proof/comment, that 768 refers to the decimal representation that has had leading zeroes between decimal point and mantissa trimmed. I updated the webrev to include a comment for MAX_NDIGITS sans both hyperlink and the foregoing verbiage: http://cr.openjdk.java.net/~bpb/8024356/ If there is any more tweaking of comments which needs to be effected prior to an approval request being posted to 7u-dev, please let me know. Thanks, Brian
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
Should we change conservative constant 1100 to optimal constant 768 ? My opinion is no (in JDK7), because the constant 1100 has lower cost of review. I mean that chances that a reviewer approves 1100 are higher than chances that [s]he approves 768. On Fri, Sep 13, 2013 at 12:49 AM, Brian Burkhalter brian.burkhal...@oracle.com wrote: On Sep 12, 2013, at 1:00 PM, David Chase wrote: On 2013-09-12, at 1:17 AM, Dmitry Nadezhin dmitry.nadez...@gmail.com wrote: The optimal constant for double conversion could be 768 , the optimal constant for float conversion could be 142, but I leave this optimization to JDK 9. It would be helpful to mention in the proof/comment, that 768 refers to the decimal representation that has had leading zeroes between decimal point and mantissa trimmed. I updated the webrev to include a comment for MAX_NDIGITS sans both hyperlink and the foregoing verbiage: http://cr.openjdk.java.net/~bpb/8024356/ If there is any more tweaking of comments which needs to be effected prior to an approval request being posted to 7u-dev, please let me know. Thanks, Brian
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
If that's the only consideration then just use 0x300 instead, which is easier to read *and* makes more sense anyway, in the context of the test. On 09/12/2013 10:13 PM, Dmitry Nadezhin wrote: Should we change conservative constant 1100 to optimal constant 768 ? My opinion is no (in JDK7), because the constant 1100 has lower cost of review. I mean that chances that a reviewer approves 1100 are higher than chances that [s]he approves 768. On Fri, Sep 13, 2013 at 12:49 AM, Brian Burkhalter brian.burkhal...@oracle.com wrote: On Sep 12, 2013, at 1:00 PM, David Chase wrote: On 2013-09-12, at 1:17 AM, Dmitry Nadezhin dmitry.nadez...@gmail.com wrote: The optimal constant for double conversion could be 768 , the optimal constant for float conversion could be 142, but I leave this optimization to JDK 9. It would be helpful to mention in the proof/comment, that 768 refers to the decimal representation that has had leading zeroes between decimal point and mantissa trimmed. I updated the webrev to include a comment for MAX_NDIGITS sans both hyperlink and the foregoing verbiage: http://cr.openjdk.java.net/~bpb/8024356/ If there is any more tweaking of comments which needs to be effected prior to an approval request being posted to 7u-dev, please let me know. Thanks, Brian -- - DML
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
For me, it is the only consideration. I'm sure in 768 because I proved it formally using ACL2 tool. On Fri, Sep 13, 2013 at 7:45 AM, David M. Lloyd david.ll...@redhat.comwrote: If that's the only consideration then just use 0x300 instead, which is easier to read *and* makes more sense anyway, in the context of the test. On 09/12/2013 10:13 PM, Dmitry Nadezhin wrote: Should we change conservative constant 1100 to optimal constant 768 ? My opinion is no (in JDK7), because the constant 1100 has lower cost of review. I mean that chances that a reviewer approves 1100 are higher than chances that [s]he approves 768. On Fri, Sep 13, 2013 at 12:49 AM, Brian Burkhalter brian.burkhal...@oracle.com wrote: On Sep 12, 2013, at 1:00 PM, David Chase wrote: On 2013-09-12, at 1:17 AM, Dmitry Nadezhin dmitry.nadez...@gmail.com wrote: The optimal constant for double conversion could be 768 , the optimal constant for float conversion could be 142, but I leave this optimization to JDK 9. It would be helpful to mention in the proof/comment, that 768 refers to the decimal representation that has had leading zeroes between decimal point and mantissa trimmed. I updated the webrev to include a comment for MAX_NDIGITS sans both hyperlink and the foregoing verbiage: http://cr.openjdk.java.net/~**bpb/8024356/http://cr.openjdk.java.net/~bpb/8024356/ If there is any more tweaking of comments which needs to be effected prior to an approval request being posted to 7u-dev, please let me know. Thanks, Brian -- - DML
Re: JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
The short answer: because it is a backport to JDK 7 of part of this JDK 8
change:
http://mail.openjdk.java.net/pipermail/core-libs-dev/2013-June/017958.html
The long answer is the theory behind the change.
Java conversion from decimal string to double is specified as if it happens
in two steps:
1) Convert decimal string to mathematical real number exactly;
2) Round the real number to nearest Java double number. If real number is
in the middle between
two adjacent Java double numbers then round to double with zero last bit.
The step between adjacent real numbers is called ULP (unit in the last
place or unit of least precision).
Each ULP segment between adjacent real numbers can be split in two half-ULP
segements.
All reals in each half-ULP segment are rounded to same Java double number.
So we can safely patch a long decimal string
when we sure that the real value of patched string lies in the same
half-ulp segment as the real value of the original string.
The above patch keeps first MAX_NDIGIT of long decimal string, discards
tail and repalces it by a single non-zero decimal digit ('1').
It is correct when the half of binary ULP of double number is a multiple of
the decimal ULP of truncated decimal string with MAX_NDIGITS kept.
When I prepared the patch I didn't try to find the optimal MAX_NDIGITS, but
I was sure that MAX_NDIGITS = 1100 is enough.
Here is an expanation:
1) If value of decimal string is larger than pow(10,309) then it is
converted to positive infinity before the test of nDigits;
2) If value of decimal string is smaller than pow(10,309) and larger than
pow(2,53) then it rounds to Java double with ulp = 2.
Half-ulp = 1.
The patch is correct when decimal ULP of kept digits is 1 or less. It is
true beacuse MAX_NDIGITS = 1100 309;
3) If value of decimal string is smaller than pow(2,53) but larger than
0.5*Doulle.MIN_VALUE = pow(2,-1022-52-1), than
binary ULP is a multiple of pow(2,-1074).
Half-ULP is a multiple of pow(2,-1075).
The patch is correct when decimal ULP of kept digits is pow(10,-1075) of
less.
pow(2,53) has 17 decimal decimal digits. MAX_NDIGITS = 1100 1075 + 17 .
4) If value of decimal string is smaller than 0.5*Double.MIN_VALUE then it
is converted to zero before the test of nDigits.
You can treat replacement of 1075 + 17 by 1100 as my paranoia.
It still was interesting for me what is the optimal truncation of decimal
string.
I made an explration after the change was accepted to JDK 8, but I want to
postpone this refinement to JDK 9.
The exploration was accompanied by a formal proof.
I used ACL2 - both a programming language and a proof tool.
http://www.cs.utexas.edu/~moore/acl2/
It's language is Lisp-like.
Here you can find definitions and the proof:
http://cr.openjdk.java.net/~bpb/nDigits/acl2/
The snipped portion of this:
; This function returns such e that all decimal digits below e can be
; be safely ignnored.
; Informally, 10^e must divide binary half-ulp
(defun find-exp (dec-exponent p q)
(declare (xargs :guard (and (integerp dec-exponent)
(integerp p) ( p 1)
(integerp q) ( q 0
(let* ((m (expt 10 (- dec-exponent 1)))
(e (expo m)))
(if (= e p) 0 (- (ulp-e m p q) 1)))
)
snipped
; Final theorem. All numbers in ( m*h, (m+1)*h ) rounds to the same
floating-point number
; if h = 10^(find-exp decexponent)
(defthmd ulp-rnd-rat-near-eq
(implies (and (integerp p) ( p 1)
(integerp q) ( q 0)
(rationalp h) ( h 0)
(integerp dec-exponent)
(rationalp x)
(= (expt 10 (- dec-exponent 1)) x)
(rationalp y)
(= (expt 10 (- dec-exponent 1)) y)
(= h (expt 10 (find-exp dec-exponent p q)))
(not (integerp (/ x h)))
(not (integerp (/ y h)))
(= (fl (/ x h)) (fl (/ y h
(= (rnd-rat x 'near p q)
(rnd-rat y 'near p q)))
:hints (
(Goal :in-theory (disable rnd-rat find-exp ulp))
(Goal' :use (:instance ulp-rnd-rat-near+-h-find-exp (x x)))
(Goal'' :use (:instance ulp-rnd-rat-near+-h-find-exp (x y)))
)
)
A function find-exp is defined above in the snipplet.
It has three arguments:
find-exp(dec-exponent,p,q) .
p and q are parameters of floating-point format.
p is number of bits in significand, q is number of bits in exponent.
Java double: p = 53, q = 11 .
Java float: p = 24, q = 8.
dec-exponent specifies a range of real numbers with the same decimal
exponent:
pow(10,dec-exponent-1) = x pow(10,dec-exponent)
The function returns the position of lowest decimal digit to be kept.
The algorithm is take m - minimal value of the range, and return binary
exponent of minimum of its binary half-ulp and 1.
The theorem says that
for any binary floating-point format with parameters p and q.
for any dec-exponent
for step h=pow(10, find-exp(dec-exponent,p,q))
for any pair of rational x and y
JDK 7u-dev review request 8024356: Double.parseDouble() is slow for long Strings
Please review at your convenience. Issue: http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=8024356 Webrev: http://cr.openjdk.java.net/~bpb/8024356/ Thanks, Brian
