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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.