Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Wed, 20 Jan 1993 13:20:44 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14318; Wed, 20 Jan 93 05:06:25 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from [192.26.234.2] by ted.cs.uidaho.edu (16.6/1.34) id AA14313; Wed, 20 Jan 93 05:06:13 -0800 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Wed, 20 Jan 93 13:04:13 GMT From: David Shepherd Message-Id: <2193.9301201304@frogland.inmos.co.uk> Subject: hol90 benchmark results To: info-hol@edu.uidaho.cs.ted (info-hol mailing list) Date: Wed, 20 Jan 1993 13:04:40 +0000 (GMT) Cc: slind@de.tu-muenchen.informatik (Konrad Slind) In-Reply-To: <93Jan19.164155met.8121@sunbroy14.informatik.tu-muenchen.de> from "Konrad Slind" at Jan 19, 93 04:41:45 pm X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 3985 If anyone pays any attentions to the benchmark figures I occassionally do on various HOl setups using the multiplier example then I have a new reference point for you. I will be the first to admit that the benchmark (i.e. the time taken for a few of what used to be the long proof steps in the multiplier verification) is not very scientific, and also as time has progressed the code to prove the multiplier has changed sligthly (e.g. one of the timed proofs in the hol90 version I've just done uses the new auto-unwind rules in one step rather than a few steps of hand coded unwindings). However it does give an overall feel of the speed of the system. Anyway, I've just started to look at hol90 and have run the benchmark on this and the result can be summed up as "WOW"!. The hol90/sml92 benchmark rating is 1789 for runtime and 2617 for runtime and garbage collect - i.e. about 18 and 26 the baseline figure of the original HOL running under Franz Lisp on a Sun3/150. Admittedly the garbage collection figure is nor strictly comparable as SML (and Allegro CL) have methods to delay collection so the big hit that gets taken later isn't included in this figure - so an 18x speed up is the relevant figure. Comparing this with hol88, my figure for a SS1+ and Allegro CL is 679 - so we have about a 2.6x speed up. Comparing with the "free" hol88 setup using AKCL from my figures brings in another speed up of about 2.4x (the difference between Allegro and AKCL) - hence hol90 looks to be about 6 times faster. Finally hol90 has benchmarked 60% faster than anything I've had before (and that was when I ran an Allegro HOL on a big Solobourne server here - for benchmarking purposes only :-). Here are the full tables. Run Time Table: Machine Lisp Hol Rating SparcStation1+ SML NJ 92 HOL90.4 1789 Solbourne 5/530 Allegro CL HOL v1.12 1114 Sparc ELC Allegro CL HOL v1.12 878 SparcStation1+ Allegro CL HOL v1.12 679 SparcServer-390 Allegro CL-sp=3 HOL88 v1.11 561 MipsMachine Allegro CL HOL88 v1.10 541 SparcStation1+ Allegro CL-sp=3 HOL88 v1.11 532 SparcStation1 Allegro CL-sp=3 HOL88 v1.11 459 Sun 3/60 Franz 38.92 HOL88 v1.01 138 T800-25 4c Franz 38.79+opt HO88 v1.11 136 Sun 3/160 Franz 38.79 HOL v0 101 Sun 3/160 Franz 38.79 HOL88 v0.9 100 Sun 3/160 Franz 42 HOL v0 96 T800-20 5c Franz 38.79+opt HO88 v0.9 76 T800-20 5c Franz 38.79 HOL v0 70 T800-20 6c Franz 38.79 HOL v0 64 Run + GC Time Table: Machine Lisp Hol Rating SparcStation1+ SML NJ 92 HOL90.4 2617 Solbourne 5/530 Allegro CL HOL v1.12 1490 Sparc ELC Allegro CL HOL v1.12 1184 SparcStation1+ Allegro CL HOL v1.12 924 SparcServer390 Allegro CL-sp=3 HOL88 v1.10 770 MipsMachine Allegro CL HOL88 v1.10 761 SparcStation1+ Allegro CL-sp=3 HOL88 v1.11 734 SparcStation1 Allegro CL-sp=3 HOL88 v1.11 633 SparcServer390 AKCL HOL88 v1.11 324 SparcStation1 AKCL HOL88 v1.05 220 Sun 3/60 Franz 38.92 HOL88 v1.01 136 T800-25 4c Franz 38.79+opt HO88 v1.11 120 Sun 3/160 Franz 42 HOL v0 115 Sun 3/160 Franz 38.79 HOL88 v0.9 100 Sun 3/160 Franz 38.79 HOL v0 92 T800-20 5c Franz 38.79 HOL v0 84 T800-20 6c Franz 38.79 HOL v0 77 T800-20 5c Franz 38.79+opt HO88 v0.9 74 SUN 3/60 AKCL HOL88 V1.05 53 ***WARNING** Comparisons involving GC can be confusing as it depends very much on amount of space alloc'ed. In particular comparisons between HOL v0 and HOL88 seem to be bogus due to differing amounts of pre-alloc'ed space. Also, Allegro CL and SML do major and minor collections so AKCL and Franz results will be worse than Allegro and SML as they haven't delayed any collection until later. NB In Allegro CL Run time include GC so actual run time is time - GC -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq Life doesn't imitate art, it imitates bad television - Husbands and Wives