Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <23857.9306211037@frogland.inmos.co.uk>
Subject: Re: HOL90 is faster, for me
To: info-hol@ted.cs.uidaho.edu (info-hol mailing list)
Date: Mon, 21 Jun 1993 11:37:24 +0100 (BST)
In-Reply-To: <199306210234.AA03906@achernar.anu.edu.au> from "Malcolm Newey" at Jun 21, 93 12:34:27 pm
Content-Type: text
Content-Length: 2092

Malcolm Newey has said:
> 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.

n.b. that's AKCL vs ACL v4 ... ACL v3 seems to have been about twice as
fast as ACL v4 for HOL ... I'm not sure how they managed to make v4
such an "improvement" :-). Hol90 was still faster than AKCL (i.e. a
sparcstation 1+ running hol90 was about 40% faster than a sparcstation
2 running hol88 on akcl)

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

Sounds similar to my experience.

Important note, if you've got a SparcStation 1 (and possibly 2) make
sure you've got a kernel that has the virtual memory fix (there's a
patch for SUNOS 4.1.1 and earlier and it should be already applied in
4.1.2) as otherwise you spend all your time paging. I've just
discovered that I'm running on an unpatched kernel when I was was sure
I'd added the the patches grrr ... on a BDD checker we found on a 15
hour run it had spent 13.5 hours in system code swapping pages *inside*
physical memory (it was on a 64Mb machine).

Final note, again from the BDD checker timings ... SparcStation 10/40's
seem like pretty neat machines :-)


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"They didn't like the rates, they don't like the poll tax,
		 and they won't like the council tax."   - Nicholas Ridley