Re: [isabelle] 64-bit Java is 6x faster than 32-bit for a recursive fibonacci



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







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