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

[Camm Maguire]

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