[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] address@hidden: Re: lstat]
From: |
Matt Kaufmann |
Subject: |
Re: [Gcl-devel] address@hidden: Re: lstat] |
Date: |
Sat, 9 Nov 2013 13:56:05 -0600 |
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
- Re: [Gcl-devel] address@hidden: Re: lstat], (continued)
- Re: [Gcl-devel] address@hidden: Re: lstat], Matt Kaufmann, 2013/11/02
- 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 <=
- 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/10
- Re: [Gcl-devel] address@hidden: Re: lstat], Matt Kaufmann, 2013/11/10