Hi, Camm -- I'm glad you got a better time result.
I notice that /v/filer4b/v11q001/acl2/camm-09-19/svn/acl2-devel/saved_acl2h was built on top of a GCL 2.6.10 ANSI dated Nov. 8. I think my run was with one built Nov. 1. Can you send me a path to your Nov. 8 build? Then I can try to re-create your result independently. With luck, I'll get the same result and we can figure that you made some nice improvement during that week, or maybe some evil computer gnomes decided to stop messing with us! Regarding your question: I think ACL2(h) uses mostly EQL has tables but has EQ and EQUAL hash tables as well. You could ask Jared to elaborate if you like (I'm not yet up to speed on the "(h)" part). -- Matt From: Camm Maguire <[email protected]> Cc: [email protected] Date: Fri, 08 Nov 2013 13:13:31 -0500 Greetings! OK, I was wrong, thankfully. Building acl2h against the gcl installed at ut gives the following times for soultions1.lisp: ; 534.05 seconds realtime, ; 514.10 seconds runtime, 9.27 seconds child runtime, ; 4.36 seconds systime, 2.90 seconds child systime. (thanks for the extended times, BTW!) I tested against two other local builds, one with C debugging only, and another with -g -O2: ; 424.69 seconds realtime, ; 408.45 seconds runtime, 5.07 seconds child runtime, ; 4.74 seconds systime, 3.13 seconds child systime. and ; 533.42 seconds realtime, ; 511.90 seconds runtime, 10.87 seconds child runtime, ; 4.50 seconds systime, 3.08 seconds child systime. respectively. This indicates to me a likely sensitivity to the hash table initialization algorithm which takes place at image build time. We already fixed a bug which had left too little randomness in our internal table. I thought we had solved this when we now initialize with gmp random numbers (256 numbers 64bits wide to hash bytes with xor). But apparently we can still learn a thing or two about hashing, and cannot blame gcc in this case. I take it these are #'eq hash tables? ============================================================================= seafoam$ diff -u solutions.lisp solutions1.lisp --- solutions.lisp 2013-11-05 10:26:43.838457000 -0600 +++ solutions1.lisp 2013-11-05 13:37:11.117399000 -0600 @@ -261,7 +261,7 @@ ; for v6-3 took about 9 minutes using ACL2(h) built on CMUCL, which is normally ; a much slower lisp than GCL. -#+(and (not cmucl) (not gcl)) +#+(and (not cmucl)) (def-gl-thm 1f :hyp (and (unsigned-byte-p 3000 x) (unsigned-byte-p 3000 y)) @@ -269,7 +269,7 @@ :g-bindings (gl::auto-bindings (:mix (:nat x 3000) (:nat y 3000)))) -#+(and cmucl (not gcl)) +#+(and cmucl) (def-gl-thm 1f :hyp (and (unsigned-byte-p 2000 x) (unsigned-byte-p 2000 y)) seafoam$ ============================================================================= I am at a loss to account for your hour long run. Ideas? My build is in /projects/acl2/camm-09-19/svn/acl2-devel/books/centaur/gl. In any case, unless I hear back from you to the contrary, I think its time to release 2.6.10. Take care, -- Camm Maguire [email protected] ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah _______________________________________________ Gcl-devel mailing list [email protected] https://lists.gnu.org/mailman/listinfo/gcl-devel
