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

[Matt Kaufmann]

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.)

That's great about the progress on hash tables.

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