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

[Matt Kaufmann]

Brilliant!  Yes, turning off sgc made the difference!  Well, in some
sense anyhow.  First consider the following input in directory
/projects/acl2/test-nov9/books/centaur/gl/, using
/projects/acl2/test-nov9/fast-linux-gcl-saved_acl2h.

(ubt! 1)
(include-book "portcullis")
:q
(si::sgc-on nil)
(lp)
(rebuild "solutions.lisp" t)
(u)
(time$ (def-gl-thm 1f
  :hyp (and (unsigned-byte-p 3000 x)
            (unsigned-byte-p 3000 y))
  :concl (equal (+ x y) (+ y x))
  :g-bindings (gl::auto-bindings (:mix (:nat x 3000)
                                       (:nat y 3000)))))

Here's the result, which I essentially got twice -- very respectable
(even though CCL is faster, recall that the "(h)" part of ACL2(h) is
highly optimized for CCL).

Time:  160.99 seconds (prove: 160.98, print: 0.01, other: 0.00)
Prover steps counted:  647
; (EV-REC *RETURN-LAST-ARG3* ...) took 
; 162.20 seconds realtime,
; 160.99 seconds runtime, 0.00 seconds child runtime,

But I also tried the following, which is the same except that sgc is
turned off a little sooner.  It ran for an hour before I killed the
job.  (Actually I essentially did that twice.)

:q
(si::sgc-on nil)
(lp)
(ubt! 1)
(include-book "portcullis")
(rebuild "solutions.lisp" t)
(u)
(time$ (def-gl-thm 1f
  :hyp (and (unsigned-byte-p 3000 x)
            (unsigned-byte-p 3000 y))
  :concl (equal (+ x y) (+ y x))
  :g-bindings (gl::auto-bindings (:mix (:nat x 3000)
                                       (:nat y 3000)))))

So in summary, this unfortunate behavior may well be related to sgc,
but can happen even when sgc is off.

By the way, I passed along to the author of the GL books your request
for info on "how other lisps might handle such things", but if that's
no longer important, let me know and I'll tell him not to bother.

Thanks for your work on 2.6.10, and good luck on this final (?)
hurdle!

-- Matt
   From: Camm Maguire <address@hidden>
   Cc: address@hidden
   Date: Sat, 09 Nov 2013 18:05:42 -0500

   Greetings, and thanks!  Looking into it now.  In case you run a check
   again, try disabling sgc and see if the problem goes away.

   Take care,

   Matt Kaufmann <address@hidden> writes:

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

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