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

[Matt Kaufmann]

Hi, Camm --

Thanks very much for rebuilding /p/bin/gcl-2.6.10pre.

Unfortunately, I'm still seeing a problem -- almost surely because I'm
using the latest svn copy of ACL2 and the books, and the so-called
"GL" books pertaining to this example have changed a lot after the
release of ACL2 Version 6.3 (which I'm guessing is what you're using).

I just killed an attempt to certify books/centaur/gl/solutions.lisp
(with the no-gcl restriction removed for the final form, "1f").
It had been running on a reasonably fast machine for more than 4 1/2
hours.  Allegro CL recently did the example in about 5.5 minutes, so
the increase in time isn't solely due to either the CCL-specific
optimizations in the "(h)" part of ACL2(h) or the fact that CCL
compiles on the fly.  I don't know if hashing is a cause.

You can play in this directory at UT CS if you like:

/projects/acl2/test-nov9/

See file README-camm in that directory for how to proceed
interactively.  (If not interested, please let me know and I'll delete
the directory.)

I'll let the GL author know what's up in case he has any ideas.

Thanks --
-- Matt
   From: Camm Maguire <address@hidden>
   Cc: address@hidden
   Date: Sat, 09 Nov 2013 08:24:37 -0500

   Greetings!

   Matt Kaufmann <address@hidden> writes:

   > Hi, Camm --
   >
   > I don't seem to have access to that gcl:
   >
   >   sloth:~% ~/camm/git/gcl/gcl/bin/gcl
   >   /u/kaufmann/camm/git/gcl/gcl/bin/gcl: Command not found.
   >   sloth:~% 
   >
   > Perhaps you'd be willing to rebuild /p/bin/gcl-2.6.10pre at UT CS, to
   > work as CLtL1 or (especially) ANSI -- then I'll just use that.  (I
   > think Gordon Novak would appreciate it too.)
   >

   Great!  Done.

   > That's great about the progress on hash tables.
   >

   We're still at ~3min and change, and ccl might still have an edge --
   have not checked on the same machine.  It does appear that this job is
   placing complex conses in compiled files.  We've put in a memoized
   hash-equal for this purpose, but we flush the table on each
   compile-file.  This flush might not be right, though I can't think of
   anything better right now.  I was wondering if you could ask the authors
   how other lisps might handle such things, in case they might know.

   Take care,

   > Thanks --
   > -- Matt
   >    From: Camm Maguire <address@hidden>
   >    Cc: address@hidden
   >    Date: Sat, 09 Nov 2013 00:04:03 -0500
   >
   >    Greetings!
   >
   >    Matt Kaufmann <address@hidden> writes:
   >
   >    > 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!
   >    >
   >
   >    saved_acl2h.gcl.ndbg was built off the nov 1 gcl installed as
   >    /p/bin/gcl-2.6.10pre.  My debugging (and other experimental) gcls used
   >    for the other tests is at ~/camm/git/gcl/gcl/bin/gcl.
   >
   >
   >    > 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).
   >
   >    Yes, this I've since gathered.  Here is the key profiling section:
   >
   >    [2]     97.7 1456.60  162.36 240851473         gethash <cycle 2> [2]
   >             159.25    0.00 2204624309/2216894685     eql1 [5]
   >               3.04    0.00 498452497/498457020     hash_eql [22]
   >               0.00    0.06   39822/45668       ihash_equal [136]
   >               0.00    0.00   19527/3180596     equal1 [40]
   >               0.00    0.00   19220/8213633     string_eq [118]
   >
   >
   >    This suggested the gethash loop itself needed work, and perhaps that the
   >    keys weren't distributed optimally, with ~10 eql calls per gethash.
   >    Backporting a few more ideas from master, I now get 
   >
   >    ; 259.47 seconds realtime,
   >    ; 228.38 seconds runtime, 9.30 seconds child runtime,
   >    ; 4.94 seconds systime, 3.42 seconds child systime.
   >
   >
   >    with the bottleneck at
   >
   >    [4]     89.2  428.53  188.98 240857323         fShash_equal <cycle 2> 
[4]
   >             186.29    0.00 1393416127/1405686504     eql1 [5]
   >               2.60    0.00 498452501/498457024     hash_eql [23]
   >
   >    I'll let you know if/when this gets pushed ...
   >
   >    Take care,
   >    -- 
   >    Camm Maguire                                        address@hidden
   >    
==========================================================================
   >    "The earth is but one country, and mankind its citizens."  --  
Baha'u'llah
   >
   >
   >
   >
   >

   -- 
   Camm Maguire                                     address@hidden
   ==========================================================================
   "The earth is but one country, and mankind its citizens."  --  Baha'u'llah