Re: [Gcl-devel] address@hidden: Re: lstat]

[Matt Kaufmann]

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 <address@hidden>
   Cc: address@hidden
   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                                     address@hidden
   ==========================================================================
   "The earth is but one country, and mankind its citizens."  --  Baha'u'llah