I would like to tell about some steps towards formal check of Raffaello's
human proof.
I work on formal verification of some Oracle projects but they are
unrelated to JDK.
In April Brian Burkhalter requested me to review the Raffaello's paper.
His paper is smart and clear but nevertheless I was afr
I think that the final webrev http://cr.openjdk.java.net/~darcy/4851642.2/
is good.
Thanks.
On Fri, Apr 15, 2016 at 8:00 AM, joe darcy wrote:
> Hi Dmitry,
>
> On 4/14/2016 7:43 PM, Dmitry Nadezhin wrote:
>
> Hi Joe,
>
> It looks good except a guard expression in the line Ma
Hi Joe,
It looks good except a guard expression in the line Math:1550
(tmp == 0.0 && a == 0.0 || b == 0.0)
Variables a and b occur asymmetrically in this expression.
A symmetrical expression would be either
(a == 0.0 || b == 0.0)
or
(product.signum() == 0)
On Fri, Apr 15, 2016 at 3:14 AM, joe dar
Joe,
Here are my comments.
1) Probably in lines StrictMath:1171, StrictMath:1220, Math:1487, Math:1593
you meant
{@code -0.0 * +0.0}
{@code -0.0f * +0.0f}
2) Lines Math:1508-1525 could be simpler:
double result = a * b + c;
return Double.isNaN(result) && Double.isFinite(a) && Doub
I'm curious to compare performance on huge numbers
between this pure Java implementation of SS and some native implementation
of SS (libgmp, for example).
On Thu, Feb 6, 2014 at 9:22 PM, Tim Buktu wrote:
> Hi,
>
> 8014320 is a JDK9 enhancement and everybody is probably busy with JDK8,
> but I
I think that better name is BigBinary.
Both BigDecimal and BigBinary are floating-point number
with radix=10 and radix=2 respectively.
More general approach is an abstract class or interface Rational
which has implementation subclasses.
Each nonzero rational number P/Q can be represented as
P/Q =
t) (first >>> 57);
> if (guard >= 128 || (result >= 0 && guard >= 128 - Character.MAX_RADIX)) {
> …
>
> provided reasonable comments were added. I understand the first part of
> this conditional, guard >= 128, but the second part eludes me. Would you
> please
&& (guard >= (1 << GUARD_BIT) || result >= 0)) {
. . .
On Fri, Dec 20, 2013 at 10:48 PM, Louis Wasserman wrote:
> @Paul Sandoz: Is there a particular reason you prefer an extra division to
> the cache?
>
>
> On Fri, Dec 20, 2013 at 8:54 AM, Dmitry Nadezh
What is performance of Long.compareUnsigned(x, y) ?
Does HotSpot implement it as a call of Long.compare(x + MIN_VALUE, y +
MIN_VALUE) or as a single machine instruction ?
On Fri, Dec 20, 2013 at 7:53 PM, Paul Sandoz wrote:
> Hi Brian,
>
> It would be nice to avoid the caches, on a hunch i am w
Time complexity of Knuth divide a/b=q approximately the same as
complexity of school multiplication b*q and is
length(b)*length(q) = length(b) * (length(a) - length(b)).
So the new heuristic seems reasonable for me.
On Sat, Nov 23, 2013 at 1:47 AM, Brian Burkhalter <
brian.burkhal...@oracle.com>
18/10/2013 17:24, Dmitry Nadezhin wrote:
>
>> The WebRev with @ignore in SymmetricRangeTests is here:
>> http://cr.openjdk.java.net/~**bpb/6910473/webrev.3/<http://cr.openjdk.java.net/~bpb/6910473/webrev.3/>
>>
>> jtreg ignores the test with a message
>> &q
;.
On Fri, Oct 18, 2013 at 2:12 PM, Alan Bateman wrote:
> On 17/10/2013 15:59, Dmitry Nadezhin wrote:
>
>> Another solution may be to exclude the SymmetricRangeTests from automatic
>> test runs,
>> and to keep this file somewhere for manual tests runs only.
>> What d
-ignore:run .
On Thu, Oct 17, 2013 at 6:59 PM, Dmitry Nadezhin
wrote:
> Another solution may be to exclude the SymmetricRangeTests from automatic
> test runs,
> and to keep this file somewhere for manual tests runs only.
> What do you think about this ?
> Can this be implemente
Another solution may be to exclude the SymmetricRangeTests from automatic
test runs,
and to keep this file somewhere for manual tests runs only.
What do you think about this ?
Can this be implemented in jtreg (for example by "@key hugeMemory" tag) ?
On Thu, Oct 17, 2013 at 2:18 PM, Alan Bateman w
Thank you, Paul.
I tried to combine your and Joe's suggestions in the updated WebRev:
http://cr.openjdk.java.net/~bpb/6910473/webrev.2/
-Dima
On Tue, Oct 15, 2013 at 12:20 PM, Paul Sandoz wrote:
> Hi,
>
> I took a look at the patch, but i am not an expert in this area.
>
> On BigInteger:
>
>
be
> documented, but I daresay most applications won't ever check for it and
> produce incorrect results as a consequence.
>
> Gili
>
>
> On 01/10/2013 2:19 PM, Dmitry Nadezhin wrote:
>
>> Dear BigInteger experts,
>> Do you have comments to my previous messa
Dear BigInteger experts,
Do you have comments to my previous message ?
http://mail.openjdk.java.net/pipermail/core-libs-dev/2013-September/021264.html
On Sat, Sep 21, 2013 at 8:13 AM, Dmitry Nadezhin
wrote:
> It is important that BigInteger objects be full-fledged instances on which
&g
It is important that BigInteger objects be full-fledged instances on which
all methods may be correctly invoked.
This bitLength bug started this discussion:
P4 JDK-6910473 : java.math.BigInteger.bitLength() may return negative "int"
on large numbers
https://bugs.openjdk.java.net/browse/JDK-6910473
w (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.
> >
> >
n 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 t
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
> wrote:
>
> The optimal constant for double conversion could be 768 ,
>
> the optimal constant for float conversion coul
n 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 () that decimal ulp should be less than 10^(-1075)
> to guarantee correctness
> ===
>
d 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
ers 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 Nadez
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)
lter <
brian.burkhal...@oracle.com> wrote:
> On Aug 27, 2013, at 7:44 PM, Dmitry Nadezhin wrote:
>
> Is it reasonable to make specification clearer ?
>
> Either to return JLS 1 specification:
> <<<
> The result is rounded to an integer by adding , taking the
sitive infinity":
<<<
Returns the closest {@code int} to the argument, with ties rounding to
positive infinity.
>>>
On Tue, Aug 27, 2013 at 3:19 AM, Brian Burkhalter <
brian.burkhal...@oracle.com> wrote:
> On Aug 26, 2013, at 7:52 AM, Guy Steele wrote:
>
> On
uld expect. For what it's worth, this is what appears to be
> implemented in the C language (GCC 4.2.1).
>
> Brian
>
> On Aug 23, 2013, at 1:44 PM, Dmitry Nadezhin wrote:
>
> > I guess that the method java.lang.Math.round() should correspond to
> > roundToInteg
= (int)a
>
> or
>
> a == (long)a
>
> so there really is no tie, unless I am missing something. The problem is
> that in the current implementation the intermediate result
>
> a + 0.5
>
> is rounded according to the IEEE standard so the conditions above are no
> l
The specification of java.lang.Math.round() says
* Returns the closest {@code int} to the argument, with ties
* rounding up.
It is not clarified what is "ties rounding up".
I guess that it should correspond to the direction "roundTiesToAway" of
IEEE 754-2008
and to the java.math.RoundingM
teger[][] pc = Arrays.copyOf(powerCache);
pc[radix] = cacheLine;
powerCache = pc; // volatile write, publish
}
return cacheLine[exponent];
}
On Wed, Jun 26, 2013 at 10:31 AM, Aleksey Shipilev <
aleksey.shipi...@oracle.com> wrote:
> On 26.06.2013, at 7:31, Dmitry Nadezhin wro
, 2013 at 11:53 PM, Aleksey Shipilev <
aleksey.shipi...@oracle.com> wrote:
> On 06/25/2013 11:36 PM, Dmitry Nadezhin wrote:
> > What about such code ?
> >
> > BigInteger getRadixConversionCache(int radix, int exponent) {
> > BigInteger retVal = null;
> &
What about such code ?
BigInteger getRadixConversionCache(int radix, int exponent) {
BigInteger retVal = null;
BigInteger[][] pc = powerCache; // volatile read
BigInteger[] cacheLine = pc[radix];
int oldSize = cacheLine.length;
if (exponent >= oldSize) {
cacheLine = Arrays.copyOf(c
, Dmitry Nadezhin wrote:
> Primitive integer types have well-specified value ranges
> byte [ -pow(2,7) , pow(2,7) )
> short [ -pow(2,15) , pow(2,15) )
> int [ -pow(2,31) , pow(2,31) )
> long [ -pow(2,63) , pow(2,63) ) .
>
> Primitive operations on these types wrap-aroun
Primitive integer types have well-specified value ranges
byte [ -pow(2,7) , pow(2,7) )
short [ -pow(2,15) , pow(2,15) )
int [ -pow(2,31) , pow(2,31) )
long [ -pow(2,63) , pow(2,63) ) .
Primitive operations on these types wrap-around in case of overflow,
but there are methods which throws Arith
pc[radix] = cacheLine;
! powerCache = pc; // publish by volatile write
! } else
! retVal = cacheLine[exponent];
return retVal;
}
/* zero[i] is a string of i consecutive zeros. */
On Sat, Jun 22, 2013 at 3:59 PM, Dmitry Nadezhin
wr
acle.com> wrote:
> On 06/22/2013 02:50 PM, Aleksey Shipilev wrote:
> > On 06/22/2013 08:06 AM, Dmitry Nadezhin wrote:
> >> Alexey,
> >>
> >> Each possible radix has its cacheLine in the cache.
> >>
> >> Cache contents looks like
> >> B
System.out.println("bitLength=" + bi.bitLength() + ";\t" +
(time1 - time0) / 1e9 + " sec\t" + (time2 - time1) / 1e9 + " sec");
}
n *= 2;
bi = bi.shiftLeft(n).add(bi);
}
}
}
On Sat, Jun 22,
Brian,
This patch significally enhances performance of string conversion for
large numbers.
I suggest to create also a fast path for power-of-two radices: 2, 4, 8, 16,
32 .
It is a simple linear algorithm that is suitable both for large and small
numbers.
Can it be attached to this bug activity
Alexey,
Each possible radix has its cacheLine in the cache.
Cache contents looks like
BigInteger[][] powerCache = new BigInteger[37] {
/*0*/ null,
/*1*/ null,
/*2*/ new BigInteger[] { 2, 4, 16, 256, 32768, ... },
/*3*/ new BigInteger[] { 3, 9, 81, ... },
/*4*/ new BigInteger[] { 4, 16, 256, ... }
Alan,
I guess that one of the reasons for all these classes
(MutableBigInteger and SignedMutableBigInteger, FDBigInteger)
is that they are mutable. The immutable class java.math.BigInteger
will require more memory allocations.
The efficient conversion from string to double has some aspects that
a
Hi Brian,
The reported benchmark results are impressive:
http://bugs.sun.com/view_bug.do?bug_id=7032154
Where can we find the 7032154 patch to review it ?
Dima
On Tue, Feb 26, 2013 at 12:50 AM, Brian Burkhalter
wrote:
> Hi Dima,
>
> On Feb 25, 2013, at 1:14 AM, Dmitry Nadezhin wro
Hi Louis,
I looked at your fix of sunbug=6358355 "Fix Float.parseFloat to round
correctly and preserve monotonicity".
https://bugs.openjdk.java.net/show_bug.cgi?id=100208
I like how you separate String->double and String->float conversions.
They both become more clear.
However I found two issues.
uppose if a
> clean build of the JDK does not complain then it is acceptable and correct.
>
> Thanks,
>
> Brian
>
> On Feb 22, 2013, at 9:41 AM, Dmitry Nadezhin wrote:
>
> So I think that the required change in FormattedFloatingDecimal is to
> delete methods
> doub
gt; Thanks,
>
> Brian
>
> On Feb 21, 2013, at 7:27 PM, Dmitry Nadezhin wrote:
>
>> Do you want that I prepare this FloatingDecimal/FormattedFloatingDecimal
>> patch ?
>>
>> -Dima
>>
>> On Fri, Feb 22, 2013 at 2:32 AM, Brian Burkhalter
>> wro
Do you want that I prepare this FloatingDecimal/FormattedFloatingDecimal patch ?
-Dima
On Fri, Feb 22, 2013 at 2:32 AM, Brian Burkhalter
wrote:
> I am withdrawing this patch for the time being as properly the changes should
> also go into the fork sun.misc.FormattedFloatingDecimal. I'll post
Hello Joe,
Thank you for the clarification.
What do you think about using BigBinary to solve the problem of a
calculation class with higher precision.
BigBinary implements arbitrary precision binary floating-point numbers
and arithmetic operations on them.
Although it rounds, the precision and ro
Your fix adds worst-case rounding tests for math functions.
It may also be useful to include worst-case rounding tests for number
conversions (string-to-double).
I have explored string-to-double issues, including problems when the
converted numbers are close to the breakpoints between doubles. T
Ulf,
I ran Caliper benchmarks on different variants of hashCode().
http://code.google.com/p/caliper/
The results and the Caliper code are below:
-Dima
- -d32 -clien
0% Scenario{vm=java -d32 -client, benchmark=HashCodeEmpty} 8,85ns; σ=0,06ns
@ 3 trials
8% Scenario{vm=java -d32 -client
On Fri, Feb 26, 2010 at 6:19 PM, Ulf Zibis wrote:
> Am 26.02.2010 12:52, schrieb Dmitry Nadezhin:
>
> I found two alternatives in the link
>> http://mail.openjdk.java.net/pipermail/coin-dev/2009-December/002618.html
>> The first alternative
>> int equalByHash
I found two alternatives in the link
http://mail.openjdk.java.net/pipermail/coin-dev/2009-December/002618.html
The first alternative
int equalByHashThreshold = 2;
public boolean equals(Object anObject) {
if (this == anObject) {
return true;
}
if (anObject instanceof String) {
Stri
In my previous post I discussed choice criteria for performance
enhancements in math libraries.
I guess that in production projects Jdk 1.6 and Jdk 1.7 the main choice
criteria is stability.
This explains why changes to math stuff in Java are almost impossible.
Here is a pair of examples:
1) T
Martin, Thank you for the answer.
I found your benchmark in "jdk/test/java/util/ArrayList".
Also I see an example of microbenchmark included in the post to
core-libs-dev:
http://mail.openjdk.java.net/pipermail/core-libs-dev/2009-November/003226.html
.
Its nice to keep such microbenchmarks in
Joe,
I'm interested in micro-benchmarking of math in OpenJDK .
This includes a choice of proper framework, a choice of representative
patterns (or testsuites).
Will math micro-benchmarking be ever hosted by OpenJDK ?
Or I should develop them elsewhere ?
-Dima
You might be interested in a rece
Jeff,
This is a really interesting link.
However, I have doubts with licensing.
The owner of this project is "omaamo".
He marked FastMath.java with LGPL v3 or later.
It seems to me that LGPL v3 is not compatible with OpenJDK's GPL v2.
OpenJDK can't include fragments of LGPL v3 code without
perm
Jeff,
I want to take a look at it, but I didn't find your post in this mailing
list.
Please give us a direct link to the FastMath sources.
-Dima
Jeff Hain wrote:
PS : The ceil and floor I posted here are an extract of a FastMath
class (I already
see some people in this mailing list inv
Jeff,
Your"ceil" and "floor" seems correct for me.
I benchmarked your code by attached benchmark program.
It is faster on some test patterns and with some Jvm options and it is
slower on some others.
Joe,
I'm curious how performance decisions are made in Jdk development process.
Are there per
f the returned
result
and monotonicity of the methods.
Suppose that there is still a bug in fdlibm 5.3 and some fdlibm function
fails to
satisfy one ulp accuracy or monotonicity. What will be the specification of
corresponding java.lang.StrictMath method in such a case ?
Joseph D. Darcy wrote:
Dm
Joseph D. Darcy wrote:
Yes, porting FDLIBM to Java has been an oft-delayed "nice to have"
project of mine. It is not obvious from looking at my ceil/floor
code, but it started with the FDLIBM versions of those algorithms.
The tests are new and greatly outnumber the code changes, as it
typica
I put a combined changeset fixing bugs 4421494 and 4396272
as comment #2 and comment #3 to OpenJDK bugzilla report:
https://bugs.openjdk.java.net/show_bug.cgi?id=100119
-Dima
Joseph D. Darcy wrote:
Dmitry Nadezhin wrote:
Hello Joe,
Thank you for the sponsorship of the bug 4421494.
I can
e JDK
?
-Dima
Dmitry Nadezhin wrote:
http://bugs.sun.com/view_bug.do?bug_id=4421494
https://bugs.openjdk.java.net/show_bug.cgi?id=100119
Summary: This old bug report says that Double.parseDouble(s) hangs
for decimal strings
in range (Double.MIN_NORMAL-0.5*Double.MIN_VALUE,Double.MIN), and
returns
inco
http://bugs.sun.com/view_bug.do?bug_id=4421494
https://bugs.openjdk.java.net/show_bug.cgi?id=100119
Summary: This old bug report says that Double.parseDouble(s) hangs for decimal
strings
in range (Double.MIN_NORMAL-0.5*Double.MIN_VALUE,Double.MIN), and returns
incorrect result for decimal string
I'm preparing a fix which restricts the range of BigInteger so that
bitLength() always
return correct result.
I can't choose between two variants of range of valid BigInteger.
A) Two's complement range
[-2^Integer.MAX_VALUE, 2^Integer.MAX_VALUE-1]
This is exactly those numbers with bitLength()
I want to make comments to this change from point of view of the post
"BigInteger.bitLength() can return negative results".
Suppose that the range of valid BigInteger is restiricted either to
[-2^Integer.MAX_VALUE , 2^Integer.MAX_VALUE-1]
or to
[-2^Integer.MAX_VALUE+1, 2^Integer.MAX_VALUE-1].
In
d) All BigInteger constructors ensure that the bit length is no
larger than 2^31 - 1;
d) is arguably the most correct approach to address the problem.
However, I think the practical consequences of this flaw are low.
Nevertheless, may I use this unimportant flaw as a lesson of Java bug
fixi
BigInteger is a class implementing arbitrary-precision integers. Of
course, it is an idealization. Let's look at implementation limits of
this type.
The bits are stored in "int[] mag" array. This sets the maximum bit
length 32*(2^31 - 1).
The "BigInteger.magSerializedForm()" converts bits to
66 matches
Mail list logo
