Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 64-bit Java is 6x faster than 32-bit for a rec...


view this post on Zulip Email Gateway (Aug 19 2022 at 14:29):

From: Gottfried Barrow <igbi@gmx.com>
Hi,

I saw 64-bit Cygwin talked about, so I send this in to show that 64-bit
Java for Cygwin would be beneficial for some things.

Basically, I've been testing a lot of different languages for a
recursive fibonacci function of this form, for a input value of 42:

fun fib (n:int) = (if (n < 2) then n else (fib(n - 1) + fib(n - 2)));

What I can say is that Scala is fast, and most everything else is slow
in comparison to it, though several things have to be taken into
consideration, such as whether a language needs to be compile, and
whether the integers are machine integers or big integers.

The crux of this email is that for Clojure, for 32-bit Java under Cygwin
or Windows, takes about 48 seconds for fib(42), where for 64-bit Java,
it's about 8 seconds, which is actually not that bad compared to other
languages.

For Isabelle/ML, fib(42) is about 4.3 seconds, though it's using big
integers.

For Scala, it's about 2.7 seconds, and the version of Java doesn't make
much difference.

For compiled Haskell, it's about 37 seconds.

For compiled Erlang, it's about 16 seconds for a pattern matched form of
fib, and 36 seconds for the if/then form.

For Julia, which is supposed to be fast, it was about 5 seconds.

For Mirah, which has syntax like Ruby, but is just a frontend on Java,
it was a little slower than Scala.

I saw Lisp SBCL, but I don't know how to compile a lisp program with it,
but http://benchmarksgame.alioth.debian.org shows that it should be
about as fast as Scala.

Many of these numbers look somewhat like what the benchmarks site shows,
other than Haskell.

I've seen a pattern emerging for me: define a datatype, then define a
fun using recursion and pattern matching for the datatype, and then do a
few calculations with the fun before proving anything.

Up front, I want to know if it works, and also I'd like to know if it's
a major loser as far as speed. A language doesn't have to be the fastest
to test that out, but if it's dramatically slower than Scala, then
that's a bad road to start down.

I've gotten the reject twice by the mail server, first because the
attachment was too big, and the second, with a smaller attachment,
probably because of the first reject. I guess Gmx is used a lot for
spam. I'll see how this one goes, but it's worth a try to put some
exposure on the possibility of 64-bit Cygwin being used. I might be
auto-banned by the auto-spam-filter-bot, which wouldn't be a bad thing.

Regards,
GB

view this post on Zulip Email Gateway (Aug 19 2022 at 14:29):

From: Gottfried Barrow <igbi@gmx.com>
Knowing nothing about concurrency, naively, this looks to me like it
would be a perfect candidate, since there are two calls to fib.

It bugs me that when calculating fib(42), the Java process only works
25% of my CPU.

Anyway, this idea makes it a higher precedence to use a language that
facilitates concurrency, like Scala, Clojure, and Erlang, though
compiled Erlang is twice as slow as Clojure.

Regards,

view this post on Zulip Email Gateway (Aug 19 2022 at 14:29):

From: Gottfried Barrow <igbi@gmx.com>
Complex things aren't that straightforward, and require talking to
oneself more than one would like.

With Scala, using BigInt, it takes 77s, and with Clojure using bigint,
it takes 21s. That assumes that things are doing what I think I've told
them to do, which means one should do one's own tests. I thought I had
read that Erlang's default integer is a machine integer, but maybe I'm
reading now that it's of arbitrary size, which means, at 16s, it would
be faster than Clojure, and arbitrary size integers is what I'd be
using. Clojure actually doesn't make you pick; it chooses what works
best. With Clojure, it's a 3megabyte jar to get the language. With
Erlang, it's a 90megabyte install.

Regards,
GB

view this post on Zulip Email Gateway (Aug 19 2022 at 14:29):

From: Makarius <makarius@sketis.net>
On Thu, 15 May 2014, Gottfried Barrow wrote:

On 14-05-15 11:23, Gottfried Barrow wrote:

fun fib (n:int) = (if (n < 2) then n else (fib(n - 1) + fib(n - 2)));

Knowing nothing about concurrency, naively, this looks to me like it
would be a perfect candidate, since there are two calls to fib.

This kind of example is generally called "micro benchmark". It is fun to
play with it, but hardly relevant in practice. There are so many
side-conditions to take into account in a real application, to say if it
is fast or not. E.g. proper integer arithmetic depends on the libray that
does that in the background, while machine integers are not integers at
all.

Just from the parallelization standpoint, the above is relatively
difficult to get performance from, and not just heat up all cores to give
you a warm feeling. You would have to do quite smart organization of the
evaluation. Some language frameworks try to do that for you, but in
general you have to do it yourself -- again depending on many
side-conditions of the overall application.

It bugs me that when calculating fib(42), the Java process only works
25% of my CPU.

Here is a version for Isabelle/ML that uses approx. 0% of CPU:

ML {*
fun fib2 f0 f1 n = if n = 1 then f1 else fib2 f1 (f0 + f1) (n - 1);
fun fib n = if n = 0 then 1 else fib2 0 1 n;
*}

See also
http://www.cs.northwestern.edu/academics/courses/110/html/fib_rec.html
which happened to be the first page Google spit out on this well-known
exercise for freshmen.

To keep this on-track for isabelle-users, I propose that you make a small
formalization in Isabelle/HOL to relate the two implementations.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 14:29):

From: Gottfried Barrow <igbi@gmx.com>
On 14-05-16 09:35, Makarius wrote:

This kind of example is generally called "micro benchmark". It is fun
to play with it, but hardly relevant in practice.

I use this to summarize, because things got long, and the long
explanation is below.

The fibonacci test is actually 100% relevant to trying to set myself up,
in the future, for evaluating how practical it is to use recursive
functions.

This would be a very relevant test for numeric computation, and that's
what I plan on doing in the future.

A starting point is to try to and find as many languages that perform
good with recursive functions that use pattern matching. If a recursive
fibonacci function isn't relevant, then why is Isabelle/HOL filled with
impractical recursive functions?

It is important, at least to me, to know how practical any particular
recursive function is. The fibonacci function would be one of the worst,
but how can I know how bad it is if I don't find the best possible
language to run it under? "Best possible" is related to how I'm
implementing mathematics in HOL.

Recursive functions will be at the very core of what I'm doing in HOL. I
want to set myself up to be able to determine what they can and can't do.

Here, you would be playing the part of the person in Mathematics
Whatever 101, saying, "Why are we doing this? Where will we ever use
this?" The application isn't always direct.

That would be one side of the coin. You're looking at the other side,
and you don't know exactly what I'm up to, so it's forgivable.

On 14-05-15 11:23, Gottfried Barrow wrote:

fun fib (n:int) = (if (n < 2) then n else (fib(n - 1) + fib(n - 2)));
This kind of example is generally called "micro benchmark". It is fun
to play with it, but hardly relevant in practice. There are so many
side-conditions to take into account in a real application, to say if
it is fast or not. E.g. proper integer arithmetic depends on the
libray that does that in the background, while machine integers are
not integers at all.

So a basic tool of rhetoric is to anticipate arguments. That would be
part of the logos, pathos, and ethos of Greek rhetoric, but 6 point
arguments on mailing lists tend to not get read, or read any where.

There's more that you could teach me than not teach me, but here it did
occur to me, before I forgot about it, to make a comment about the
narrowness of what I'm doing.

The context is the prolific use, by many, of using recursive functions
that use pattern matching in Isabelle/HOL.

I know that recursive functions are bad performers, and recursive
functions with pattern matching are even worse. I've become a follower
of the HOL crowd. I use recursion and pattern matching, and my
inclination is to use it as a first choice over if/then/else.

Consequently, my picking the fibonacci function is totally relevant to
testing languages to see how they perform under worst case conditions.
It is a micro benchmark, but it's the one single test to test languages
for what's on my mind, the use of recursive functions in HOL, and how
they will play out when trying to run them with a programming language.

There's always more context than can be explained. What I'm doing is
"the big pursuit of all fast, probably functional, programming languages
that sync up good with how I implement logic in HOL." That language is
actually ML, but for some reason, I think I need another one in addition
to it.

It's very time consuming. I find a language. I look at the docs on the
web to try to determine if it has the basic requirements, which is the
ability to curry or do partial application, pattern matching, and the
ability to define datatypes. I download it. I figure out how to write
the fibonocci function. I try to find out what kind of integers it's
using by default. I time it multiple times. More.

There are so many side-conditions to take into account in a real
application, to say if it is fast or not.

I did mention that it can be hard to know if a test is meaningful. If
I'm trying to test 20 languages, it's not that I know that I proved
something is slow, but fast generally always means something, especially
after I've started to see some patterns emerging, like that out of 20
languages, none of them run faster than about 6 seconds for fib(42), and
that ML is performing the best, at about 4.5 seconds.

I give two examples where I got mislead. I judged Scala as fast, and was
using it as a benchmark, but when I switched to big integers, it got
really slow.

I judged JRuby really slow, but when I switch to running it under 64-bit
Java, fib(42) went from 51s to 23s, whee 23s isn't that bad relative to
what I've seen

I just got through installing Rust. It fit that pattern of being a
compiled language that's better than most, but not better than ML. It
ran fib(42) at about 6 seconds, which is good.

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.

I have to make the best possible conclusions given a limited amount of
time. Isabelle/ML was #2 as the benchmark until I saw that Scala when
from 2.7s to about 70s, so now ML is the benchmark, and it helps me
something to compare other languages to.

It bugs me that when calculating fib(42), the Java process only works
25% of my CPU.

Here is a version for Isabelle/ML that uses approx. 0% of CPU:

The anticipation of arguments would have saved us some time. I already
had 3 other fast fibonacci functions.

If Ruby is fast at three out of 4 fibonacci functions, does that make
Ruby fast? No, it's slow, though like I say, it wasn't as slow as I thought.

See also
http://www.cs.northwestern.edu/academics/courses/110/html/fib_rec.html
which happened to be the first page Google spit out on this well-known
exercise for freshmen.

Am I insulted? I'm always insulted, but I control myself, and I
understand that I'm a freshman in the big ocean of life on the terra firma.

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.

Regards,
GB

view this post on Zulip Email Gateway (Aug 19 2022 at 14:29):

From: Makarius <makarius@sketis.net>
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.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 14:29):

From: Makarius <makarius@sketis.net>
On Fri, 16 May 2014, Gottfried Barrow wrote:

A starting point is to try to and find as many languages that perform
good with recursive functions that use pattern matching.

You should look in the vicinity of ML and Haskell. The latter is
particularly well-known to beat most other languages in the usual
benchmarks.

If a recursive fibonacci function isn't relevant, then why is
Isabelle/HOL filled with impractical recursive functions?

There is nothing impractical about recursion. The slowness of the naive
fibonacci implementation is caused by the non-linearity of the invocation,
which causes an exponential blowup. But the slightly tuned linear
implementation demonstrates that the complexity is actually not there.

What is nice about a mathematical language like Isabelle/HOL is that you
don't have to care about complexity. You just do symbolic reasoning, and
you can e.g. make some equivalence proof of a term that represents the
naive implementation to the tuned one. Then you give the latter to the
code generator to run it on the machine.

I know that recursive functions are bad performers, and recursive functions
with pattern matching are even worse.

This was disproven in the 1980s or so, when the first efficient
implementations of ML came about. Recursion without pattern matching was
already known to be efficient much earlier, in the olden days of LISP.

It is just due to technical accidents in C or Java that these guys are
still lagging begind some decades. The Scala guys have to play a lot of
funny tricks to cope with the tiny constant-sized stack on the JVM and
lack of tail recursion.

In Poly/ML you can be relaxed about this, and allocate hundreds of MB or
some GB of stack without too much worrying, or no stack at all if written
slightly differently. But the art of tail-call optimization is often
irrelevant these days.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 14:29):

From: Gottfried Barrow <igbi@gmx.com>
Richard,

Thanks for the info from James McDonald. I was confused about SBCL. I
had installed it, but I thought the instructions on how to build it was
part of what to do to compile a script. When sorting through 20
languages, unfamiliarity and some resistance can cause me to abandon
testing a language out.

This worked out better, because I hadn't downloaded the newest version
for Windows.

With SBCL on Windows, with the default options, I get 5.6 seconds for
fixnum, and 9.8 seconds for integer. I'm running a 2.8GHz old quad core,
where it only utilizes 25% of the cpu when it's running the program.

Where SBCL really separates itself is with big integers, because fib(42)
is only 4807526976. That wasn't forcing these other languages to use
non-machine integers, the ones that don't make you choose. I say more
about that in my reply to Makarius.

Regards,
GB

view this post on Zulip Email Gateway (Aug 19 2022 at 14:30):

From: Richard Waldinger <waldinger@AI.SRI.COM>
from jim mcdonald (cc-ed):

view this post on Zulip Email Gateway (Aug 19 2022 at 14:30):

From: James McDonald <mcdonald@kestrel.edu>
[re-sending from jlm—-r]

More generally, if you are really trying to benchmark various languages and implementations,
you might want to consider a broader suite of tests. E.g., within the lisp world, you could
look at Dick Gabriel’s “Performance and Evaluation of Lisp Systems” from around 1985.
(http://www.dreamsongs.com/NewFiles/Timrep.pdf)

In particular, if your focus is on function call overhead, the TAK and PUZZLE tests might
be of interest, including the variants that move things around to account for cache lines.

jlm

view this post on Zulip Email Gateway (Aug 19 2022 at 14:30):

From: Gottfried Barrow <igbi@gmx.com>
On 14-05-17 18:25, James McDonald wrote:

More generally, if you are really trying to benchmark various
languages and implementations,
you might want to consider a broader suite of tests. E.g., within
the lisp world, you could
look at Dick Gabriel’s “Performance and Evaluation of Lisp Systems”
from around 1985.
(http://www.dreamsongs.com/NewFiles/Timrep.pdf)

James (and Makarius below),

Thanks for the specific optimizations. Right now, I'm doing rough
comparisons between languages, but all that could come in handy if I go
the Lisp route, and I'm not seeing anything other than the Lisps that
don't tend to get slaughtered by big integers, though Lisp may get
slaughtered in other ways. I wouldn't know.

And thanks for the PDF link also. I used the TAK test out of it, since
it was short and easy.

I show times for Isabelle/ML, Haskell, SBCL, Clojure, Scala, and JRuby,
three of them with both a 32-bit and 64-bit version. At least for the
three tests, SBCL comes out ahead overall. Enough to warrant more
looking in to.

http://github.com/gc44/prelim/tree/master/1400/1405A_bigint_prog_lang_perf_tests

On 14-05-16 15:44, Makarius wrote:

On Fri, 16 May 2014, Gottfried Barrow wrote:

A starting point is to try to and find as many languages that perform
good with recursive functions that use pattern matching.
You should look in the vicinity of ML and Haskell. The latter is
particularly well-known to beat most other languages in the usual
benchmarks.

This is where it pays to sometimes do my own tests. I've searched
multiple times to get comparisons between Scala and Haskell. I've read
repeatedly, and seen on the benchmark sites, that Haskell is comparable,
but a little slower than Scala.

Obviously, they're not talking about the Windows 32-bit version, because
it's slow. Not a little slow, but a lot slow, relative to my own limited
tests. I show that on pages at the link above.

If a recursive fibonacci function isn't relevant, then why is
Isabelle/HOL filled with impractical recursive functions?
There is nothing impractical about recursion. The slowness of the
naive fibonacci implementation is caused by the non-linearity of the
invocation, which causes an exponential blowup.

But surely blowups are good for stress tests.

I know that recursive functions are bad performers, and recursive
functions with pattern matching are even worse.
This was disproven in the 1980s or so, when the first efficient
implementations of ML came about. Recursion without pattern matching
was already known to be efficient much earlier, in the olden days of
LISP.

I believe you, but "implementation" is the key word, where
"implementation" is on my mind only because some Stackoverflow answerer
was making sure everyone knows that languages aren't slow, but
implementations are slow. Coming from that guy it was very irritating.
Coming from me, it's profound.

I've been doing two things on multiple languages. Running the if/then
form of the fibonacci function, and then hunting down how to do it with
pattern matching. Most of the time, pattern matching has been slower.

It was even slower for Haskell. I'm looking right now at where I put the
time in filenames, that it was 36s for if/then/else, and 51s for pattern
matching. But the Windows 32-bit version of HaskellPlatform is slow.
It's messed up, so that may not mean anything. I check these things
multiple times, and want to check them again, because it's easy to get
confused in all the details.

With Erlang, on the other hand, it was significantly faster with pattern
matching. I don't think they even have a normal if/then/else statement.

I want as much speed as possible, because I think I'll need it.

I have two datatypes I want to test out, at least at some point, that
point not being way off in the future. My first guess is that one of
them will be slow, but I need to find out, to make some decisions.

I added two more tests, so now I'm doing three times more testing than
what I was doing, which is infinitely more than what I was doing before,
which, though not zero, was still only a small number infinitely close
to zero, call it epsilon.

I thought about things a little more because you brought these things
up, but there's no room for that here.

Regards,
GB


Last updated: Apr 25 2024 at 04:18 UTC