record performance for Shen Prolog on HP Envy under Chez-Scheme port

[dr.mt...@gmail.com]

Testing Einstein's riddle for 10 iterations gave a performance of 7.16 MLips so kudos to the HP engineers, Chez Scheme people, Bruno's port and the S kernel.

That's about 3X the performance of the old machine.

Yay

Mark

[dr.mt...@gmail.com]

SBCL port is nearly 4X slower.

M.

[dr.mt...@gmail.com]

I'm old enough to remember when Prolog was C Prolog on a VAX 11/750 running about 1 KLIP.

In 1990 we got a Prolog machine from ICL called the KCM or Knowledge Crunching Machine

which ran at 750 KLIPS.   Probably top end then for a commercial Prolog on a work

station was about 120 KLIPS.  But people did good work with this technology.   There

 is a paper https://dl.acm.org/doi/pdf/10.1145/74925.74947 on the KCM and at the

back you'll see the times.   Quintus did 60 KLIPS on a 25Mhz machine which ballpark

terms translates today to 2.5 MLIPS per Ghz.   And that's a Prolog that was coded at a very

low level.

7.16 MLIPS is very good for a Prolog that is designed to run on just about any platform

you like and which will talk with the native host and uses occur check.  Because of the small size and the 

garbage collector of the S series you could actually run it in an embedded device.

Somebody asked me why the performance jump.  It's the machine.  The software has not

changed, but the software was fast before the machine was swapped out.   The clock speed

of the new machine is actually slightly lower than the old.

M.

[nha...@gmail.com]

I suspect that Prolog implemented on top of Chez can maybe outperform SWI.

Shen prolog compiler does basically no Prolog specific optimizations, so there must be a lot of room for improvement.

Mark Thom may be able to give some advice after finishing Scryer prolog.

[dr.mt...@gmail.com]

I've been testing FTP 34 (Fast Theorem Prover) using the new machine on

equivalential calculus problems.    Same Scheme/Shen platform.

(14-) (ftp.<-kb (ec))

run time: 0.46875 secs
5972798 inferences
true

which includes computing and dispatching generated proof attached.   That's nearly 12.75 MLips.

Its about 6X what I could reach before.

In the pre-S kernels there was a file optimise.lsp which optimised many low level Prolog operations

by overwriting the Shen but I felt no need in the S series.  Whether such a file would push the boundary

even further, I do not know.

M.

[dr.mt...@gmail.com]

Beaten the last record; this from group theory

(62-) !60
(.<-kb [all a [all x [[eq [+ a x] e] => [eq a [inv x]]]]])

run time: 1.6875 secs
22438660 inferences
true

Axioms (eq is equality)

[[all x [all y [all z [eq [+ x [+ y z]] [+ [+ x y] z]]]]]
       [all x [eq [+ e x] x]]
       [all x [eq [+ x e] x]]
       [all x [eq [+ x [inv x]] e]]]

About 13.3 MLips; proof below.

M.

[dr.mt...@gmail.com]

Again broken the record  > 20 MLips.

run time: 0.296875 secs
5980233 inferences
true : boolean

M.

[Mark Tarver]

run time: 0.25 secs
6623310 inferences
true : boolean

> 26 MLips

prove the following group theory theorem

(<-kb [all x [eq [inv [inv x]] x]]) 

M.

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/8b840c4b-9dea-43a0-a887-286cec2116b8n%40googlegroups.com.

[dr.mt...@gmail.com]

Comparison to SWI Prolog on naive reverse

6 ?- time(test(10000)).
% 2,320,000 inferences, 0.062 CPU in 0.053 seconds (117% CPU, 37120000 Lips)

That's not such a huge gap actually between SWI Prolog and Shen Prolog - about a factor of 2.  

M,