Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Date: Mon, 21 Jun 1993 12:34:27 +1000
From: Malcolm Newey <Malcolm.Newey@cs.anu.edu.au>
Message-Id: <199306210234.AA03906@achernar.anu.edu.au>
To: info-hol@ted.cs.uidaho.edu
Subject: HOL90 is faster, for me


Here's a little something for those of you who lie awake wondering
whether to make the switch to HOL90.  There does seem to be scope for
making SOME HOL activities substantially more efficient by migrating
them to the newer system.

In mail to info-hol on Jan. 20, David Shepherd exclaimed "WOW" at the
speedup he got on his first benchmark of HOL90, but after the dust had
settled we found him more subdued;  he had been set straight on the
advantages of version 2 of HOL88.  He concluded on Jun 21 that

        a) hol90 is marginally faster than hol88 v2.01 compiled using
           ACL (Franz's Allegro Common Lisp),  and
        b) that AKCL is slower than ACL, so that hol90 is the fastest
           of the `free HOLs'.

Konrad Slind's contribution that day is worth repeating

> ..... As always, do your own tests on your own problems and remember
> the saying "There's lies, damn lies, and then there's benchmarks".

John Van Tassel's recent expose on ACL version 4, supported by David
Shepherd (info-hol, May 12), seems to show that the free version of
HOL88 (the one sitting on AKCL) is as good as one can hope for.  He
found that AKCL is over twice the speed of ACL.

Since I recently took the plunge and converted two nontrivial HOL
packages to HOL90, I have taken Konrad's advice and produced my own
figures on machines that I habitually use.  What I find most interesting
is how different the results are for the two applications.


Application A - 5000 lines of HOL source code;

   Sun model   Sun rating      hol88 time      hol90 time      speedup

   4/75        28 Mips         1858 sec         612 sec         3.0
   4/40        16 Mips         2821 sec         949 sec         3.0
   SLC         12 Mips         3275 sec        1111 sec         2.9
   4/110        7 Mips         4748 sec        1140 sec         4.2


Application B - 2600 lines of HOL source code;

   Sun model   Sun rating      hol88 time      hol90 time      speedup

   4/75        28 Mips         1250 sec         209 sec         6.0
   4/40        16 Mips         1974 sec         351 sec         5.6
   SLC         12 Mips         2312 sec         401 sec         5.8
   4/110        7 Mips         3297 sec         405 sec         8.1


(In each case the machine used was lightly loaded.  Tests were repeatable;
each case was run at least twice and results differed by few seconds.  The
tolerance on the speedup figures for each situation is about 0.1)

The times were derived using the standard C-shell time function and so are
`just' run-times.  They do, however, mirror elapsed times; - except that my
desktop 16MB Sun/SLC pages almost continually when running anything significant
in HOL90; on this machine, I lose much of the advantage of HOL90.

  From the above results, one can extract estimates of the speedup one
would get by upgrading one's machine.  However, for no pair of machines
in the study was the increase (that was actually achieved) as great as
the standard Mips rating suggests.

The difference in speedups between applications A & B was startling
because each is a large collection of rule and tactic invocations (mostly
by one person) and so I expected it to behave as a "typical HOL script".
The one significant difference between the two (that I can think of) is
that, in application B, I often use rewriting with quite large rule sets
(over 100 theorems).

Lessons:

1) In one `typical' situation HOL90 was found to be 3 times as fast as
   HOL88 v2.01 (AKCL).  In a similar situation it was 6 times as fast.
   Slind's Rule is supported - "Do your own tests on your own problems".

2) Don't expect to achieve a doubling in speed by buying a machine
   with twice the Mips rating.

3) Make sure you have enough memory (as determined by experiment) or you
   can lose the advantage that you might otherwise gain by going to HOL90.