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

[Matt Kaufmann]

Well....

I tried to reproduce it, and I didn't exactly: the run finished but
took quite a long time.  I left sgc on for the entire run.

; 1434.17 seconds realtime,
; 1429.34 seconds runtime, 0.00 seconds child runtime,
; 1.12 seconds systime, 0.00 seconds child systime.

That compares with what I got with the "fast" build, as reported
before (sorry, I'd left off the third line before), but note that (as
I mentioned previously) it had sgc turned off at a suitable point.

; 162.20 seconds realtime,
; 160.99 seconds runtime, 0.00 seconds child runtime,
; 0.85 seconds systime, 0.00 seconds child systime.

I don't know what to conclude from this.  I was probably using a
different machine, if you were using seafoam; but both are Intel Xeon
3.50GHz machines, though they could conceivably have different
relevant software installed.  Given my previously reported result,
where turning off sgc at an earlier point ruins the run, I naturally
suspect that the garbage collector is to blame.  I don't have your
knowledge of Lisp implementation, of course, so I'll stop there.

>> Perhaps you have some insight on what is not compiled in the
>> fast build that could be relevant.

The "fast" build is so called because it avoids compiling certain
built-in auxiliary functions (we call them "*1* functions", but no
matter) during ACL2's boot-strapping procedure.  All such functions
are compiled again at the end of ACL2's initialization in any case, so
I can't see that "fast" vs. "slow" makes any difference, other than to
tweak the memory image in a way that I'd normally expect to be
irrelevant.

I've saved a log in file
/projects/acl2/test-nov9/books/centaur/gl/matt-nov10-11am.log, in case
you care to try to reproduce this behavior.  Actually, you won't need
to look at it -- I'll just tell you what I did.  First I built ACL2
like this in directory /projects/acl2/test-nov9/:

(time nice make PREFIX=gcl- LISP=./gcl-ansi ACL2_HONS=h) >& make-gcl-hons.log&

[The only error was in trying to write backup files to saved/ -- I no
 longer have the necessary permissions.  If you would, please do the
 following, ignoring permission errors you get in the output:
 chmod -R g+w /projects/acl2/test-nov9
]

Then I did the following in directory
/projects/acl2/test-nov9/books/centaur/gl/:

/projects/acl2/test-nov9/gcl-saved_acl2h
(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)))))

-- Matt
   From: Camm Maguire <address@hidden>
   Cc: address@hidden
   Date: Sun, 10 Nov 2013 11:38:36 -0500

   Greetings!  Can you reproduce this in a non 'fast-build'?  I can't.
   There must be more to it than this though if sgc off affects the
   problem.  Perhaps you have some insight on what is not compiled in the
   fast build that could be relevant.

   /projects/acl2/test-nov9/saved_acl2h.gcl -- against
   /p/bin/gcl-2.6.10pre, slow build, 180.88 seconds for solutions.lisp.

   /projects/acl2/test-nov9/saved_acl2h.gcl.fgdb -- against
   /home/camm/git/gcl/gcl/bin/gcl (debugging), fast build, hang

   /projects/acl2/test-nov9/saved_acl2h.gcl.gdb -- against
   /home/camm/git/gcl/gcl/bin/gcl (debugging), slow build, 440.84 for
   solutions.lisp.

   I guess if the slow builds are completely reliable, this issue might be
   moot re: gcl release.

   Take care,

   Matt Kaufmann <address@hidden> writes:

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

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