Re: [isabelle] 64-bit Java is 6x faster than 32-bit for a recursive fibonacci
On Fri, 16 May 2014, Gottfried Barrow wrote:
The big question is always whether a language is using machine integers
or big integers. If I know that a language is using machine integers,
and it runs at fib(42) at 6 seconds, that's alright, but not that
impressive, since ML uses arbitrary size ints, though it could be
optimizing, by using machine ints until it needs big ints.
Yes, this is the rather obvious thing that David Matthews is doing here
for decades. I always wondered why that is not done everywhere, until
some years ago some knowledable people explained to me the reason:
compatibility with the C programming model.
So C is the reason for Java bigints being so slow, because they are always
big, even for small numbers.
To keep this on-track for isabelle-users, I propose that you make a small
formalization in Isabelle/HOL to relate the two implementations.
I thought it was somewhat on track. I've shown an example that 32-bit
Java can be up to 6x slower than 64-bit Java, so 64-bit Java would be a
good reason to try and get 64-bit Cygwin going, not that I expect that.
Many times I've assumed that there's not a real benefit to 32-bit
programs, but I've shown there is.
That is actually in the center of isabelle-users in a technical sense: we
have this mix of supported platforms (Linux, Windows, Mac OS X) and
programming language environments (e.g. Poly/ML, Scala/JVM, certain
C-implemented tools on Cygwin).
So what is the best adjustment of the 32 vs. 64bit switch? The answer
depends on many side-conditions.
For the Prover IDE a 64bit JVM could actually be beneficial, but it is not
used on Windows due to some other side-conditions. 64-bit Cygwin is
unrelated to that, because it is Windows-Java not Cygwin-Java.
From the subject of your initial mail, I was actually expecting some
problem report that PIDE no longer works on your machine with only 32-bit
Java. The micro-benchmarks are a rather relaxing contrast to that
This archive was generated by a fusion of
Pipermail (Mailman edition) and