[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] address@hidden: Re: lstat]
From: |
Camm Maguire |
Subject: |
Re: [Gcl-devel] address@hidden: Re: lstat] |
Date: |
Sat, 09 Nov 2013 18:05:42 -0500 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux) |
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
- Re: [Gcl-devel] address@hidden: Re: lstat], (continued)
- Re: [Gcl-devel] address@hidden: Re: lstat], Camm Maguire, 2013/11/04
- Re: [Gcl-devel] address@hidden: Re: lstat], Matt Kaufmann, 2013/11/05
- Message not available
- Message not available
- Message not available
- Message not available
- Message not available
- Message not available
- Message not available
- Message not available
- Message not available
- Message not available
- Message not available
- Re: [Gcl-devel] address@hidden: Re: lstat], Camm Maguire, 2013/11/08
- Re: [Gcl-devel] address@hidden: Re: lstat], Matt Kaufmann, 2013/11/08
- Re: [Gcl-devel] address@hidden: Re: lstat], Camm Maguire, 2013/11/09
- Re: [Gcl-devel] address@hidden: Re: lstat], Matt Kaufmann, 2013/11/09
- Re: [Gcl-devel] address@hidden: Re: lstat], Camm Maguire, 2013/11/09
- Re: [Gcl-devel] address@hidden: Re: lstat], Matt Kaufmann, 2013/11/09
- Re: [Gcl-devel] address@hidden: Re: lstat],
Camm Maguire <=
- Re: [Gcl-devel] address@hidden: Re: lstat], Matt Kaufmann, 2013/11/09
- Re: [Gcl-devel] address@hidden: Re: lstat], Camm Maguire, 2013/11/10
- Re: [Gcl-devel] address@hidden: Re: lstat], Matt Kaufmann, 2013/11/10