[MLton-devel] Twelf Performance Comparison (ad hoc)

[Frank Pfenning]

Summary: MLton wins big on one significant example with
standard settings.

Background: After a message by Chris Richards about the
problems with SML/NJ, versions > 110.40 [hope I got that
right], I made Twelf SML'97 Standard compliant and ported
the few extensions so it would work under

  SML/NJ 110.0.3  [that's what I have used so far at CMU]
  SML/NJ 110.40   [used at Princeton?]
  Poly/ML 4.1.3
  MLton 20020923

All of these were used "out of the box" with default
settings.  I haven't tried Moscow/ML or SML.NET.

The example I used was a memory leak found by Karl Crary
using his formalization of TALT (Typed Assembly Language
Two) in Twelf.  It turned out in the end the leak could not
be easily fixed, although it could be ameliorated somewhat.

Here are the summary times for successive runs of Karl's
suite on the 4 different SML implementations above.  Since
computation is memory-bound (and in Twelf it often is),
these running times depend very critically on the available
memory, which means high standard deviation for multiple
runs depending on how many other processes are running, etc.

Reported is total run time, not wall-clock time.  However,
the wall clock times are very close to the reported times.
SML/NJ and MLton also break out the GC times, but not
Poly/ML, so I haven't listed them here.  "?" means I didn't
bother running or waiting for this experiment.  The way this
example works is that one loads a signature and then defines
a proof term using that signature, multiple times (#1 is
first run, #5 is fifth run of the same term).  The proof
term is being stored each time, and shadowed terms cannot be
garbage collected, which is where the memory leak comes
from.

Here are the numbers:

                #1	#2      #3     #4       #5
SML/NJ 110.0.3  24.460	24.490  77.660 484.930    ?
SML/NJ 110.40   13.771  38.188 176.690   ?        ?
Poly/ML 4.1.3   34.320  53.410  75.810 102.900  128.250
MLton 20020923   6.500   7.860   6.330  15.800    6.680

I believe I am using Linux Red Hat 7.1 kernel 2.4.18 (if that makes
any sense) with 512 MB memory.  I can't actually tell you
my processor speed---what is the best way to find these
things out under Linux?

Note that performance of SML/NJ 110.0.3 and 110.40 degrades
essentially exponentially, with SML/NJ 110.40 being almost
twice as fast initially.

Poly/ML degrades almost linearly.

MLton does not degrade at all, although at some point in the
middle (#4) it does some expensive garbage collection (the added
time is all in gc).

I don't really have an explanation for these numbers, but
they strongly suggest Karl might benefit for working with
MLton.

Since the standard test suite runs, I plan to check the new
versions into the repository tomorrow, after some cleanup.
At that point I can make it available on the Twelf web page
as an unofficial working version.  Karl would have to give
permission before I give out his snapshot code, but there
will be other test suites available.

  - Frank


-------------------------------------------------------
This SF.NET email is sponsored by:  The Best Geek Holiday Gifts!
Time is running out!  Thinkgeek.com has the coolest gifts for
your favorite geek.   Let your fingers do the typing.   Visit Now.
T H I N K G E E K . C O M        http://www.thinkgeek.com/sf/
_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel