Greetings! Before we look further, let me run this in gdb. I have
encountered situations in which the gprof profilier fails to detect the
end of certain (optimized, inlined) functions and misreports the
statistics. More later when I get this done.
Matt, I was trying the same in ccl just to see where we stand, and could
not load the portcullis. Do you happen to have a comparable ccl time
for this handy?
Take care,
Matt Kaufmann <kaufm...@cs.utexas.edu> writes:
> Hi, Jared and Camm --
>
> I ran the experiment you suggested, Jared (thanks for the suggestion).
> In books/centaur/gl/:
>
> (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)))))
>
> That took 78 seconds (a very nice improvement!). Then:
>
> ACL2 !>:q
>
> Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
> ACL2>(hons-summary)
>
> Normed Objects Summary
>
> - NIL-HT: 4 count, 5,000 size ( 0.08% full)
> - CDR-HT: 9,071,974 count, 12,974,622 size (69.92% full)
> - CDR-HT-EQL: 0 count, 1,000 size ( 0.00% full)
> - STR-HT: 1 count, 1,000 size ( 0.10% full)
> - PERSIST-HT: 0 count, 100 size ( 0.00% full)
> - FAL-HT: 0 count, 1,000 size ( 0.00% full)
>
> NIL
>
> ACL2>(hl-hspace-str-ht *default-hs*)
>
> #<hash-table 0000000004e06af0>
>
> ACL2>
>
> (I did some searching and did find another 'equal hash table besides
> that str-ht, namely; *hcomp-book-ht*, but it's quite small and not
> relevant here.)
>
> So I'm again stumped, since the cdr-ht is, I think, an 'eq hash
> table.
>
> Camm, is there a way to identify the callers that are setting a hash
> table with test 'equal? The profile you sent seems to be at the level
> of C, so I don't know what to trace.
>
> -- Matt
> From: "Jared C. Davis" <ja...@cs.utexas.edu>
> Date: Mon, 11 Nov 2013 16:18:24 -0600
> Cc: Camm Maguire <c...@maguirefamily.org>,
> "GCL-devel@gnu.org" <gcl-devel@gnu.org>
>
> Hi,
>
> I believe Matt is correct that the only use of EQUAL hash tables in
> the (h) part of ACL2(h) is for string hashing. In fact, for the most
> part, in a single-threaded context, I think there should typically be
> just a single string hash table.
>
> At the relevant part of your benchmark, you might run (hons-summary)
> to see the size and count of this table, in case that's helpful. Or
> if you want to get your hands on the hash table to really take a deep
> look at it, you can try, e.g.,:
>
> ACL2 !>(hons "foo" "bar")
> ("foo" . "bar")
> ACL2 !>:q
> :q
>
> Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
> ? (hl-hspace-str-ht *default-hs*)
> #<HASH-TABLE :TEST EQUAL size 2/1000 #x30200EA5441D>
>
> Cheers,
> Jared
>
> On Mon, Nov 11, 2013 at 3:21 PM, Matt Kaufmann <kaufm...@cs.utexas.edu>
> wrote:
> > Hi, Camm --
> >
> > That's interesting, but I'm confused, and I'm definitely not an expert
> > on hash tables. I looked at the files that implement the "(h)" part
> > of ACL2(h), which is almost certainly what is involving hash tables,
> > and it looks to me like maybe the only 'equal hash tables are for
> > strings.
> >
> > I'm forwarding this to Jared, since he is the most recent author of
> > that code (plus, you mention him as helping with potentially related
> > reader issues), in case he has time to shed light on this.
> >
> > -- Matt
> > From: Camm Maguire <c...@maguirefamily.org>
> > Date: Mon, 11 Nov 2013 12:49:41 -0500
> >
> > Greetings!
> >
> > Just a followup -- the remaining time appears to be in sethash for an
> > 'equal hash-table:
> >
> >
> =============================================================================
> > index % time self children called name
> > 103979625 sethash [1]
> > [1] 84.2 2.11 49.03 0+103979625 sethash [1]
> > 22.58 6.16 167566772/167566772 fShash_equal [2]
> > 0.00 20.28 119656/131885 alloc_relblock [6]
> > 0.01 0.00 119656/205048 alloc_object [47]
> > 103979625 sethash [1]
> > -----------------------------------------------
> > 22.58 6.16 167566772/167566772 sethash [1]
> > [2] 47.3 22.58 6.16 167566772 fShash_equal [2]
> > 5.25 0.00 363849475/363849475 hash_eql [12]
> > 0.91 0.00 1174935219/1174940911 eql1 [18]
> > 0.00 0.00 12/2577623 Fand <cycle 2> [151]
> > -----------------------------------------------
> > 0.29 5.78 3/14 make_cons [9]
> > 1.06 21.19 11/14 alloc_relblock [6]
> > [3] 46.6 1.35 26.97 14 GBC [3]
> > 26.93 0.00 25304834/25331171 sgc_mark_object1
> <cycle 1> [5]
> >
> =============================================================================
> >
> > This is somewhat remarkable, as the 'eql gethash calls which greatly
> > dominate in number are no longer on the radar. Presumably the
> algorithm
> > makes some complex cons, (definitely not your grandmother's '(1 2 3)
> > list), uses an 'equal hashtable to make it equal-unique, and then uses
> > that as a key in an 'eql hashtable for the real heavy work.
> >
> > This just reminded me of the work we did earlier regarding the loading
> > of complex conses in compiled files, which overloaded the #= reader
> > until we memoized the routine calculating the hash-equal index. This
> is
> > barely necessary to the gcl compiler -- the point is to catch errors
> > where the constant list to be compiled in changes during compilation.
> > And as I indicated earlier, we flush the memoizing hash tables on each
> > compile-file. This, together with the implementation of the 'hybrid'
> #=
> > algorithm suggested by Jared, made the loading of these conses very
> > fast.
> >
> > My question is if we've learned anything which might make the above
> > results yet faster. By default, the hash-equal index descends no more
> > than three levels, car and cdr, into a cons to xor up the index. It
> > does not attempt to descend the entire structure memoizing as one goes
> > like the compiler version. There the depth limit is much greater
> (1000)
> > due to its purpose and the absence of any table. My intuition tells
> me
> > that there is no way a memoized version of the generic hash-equal
> would
> > pay off. It seems we would have to flush on each call, or never. It
> > would only speed up index calculations of great depth, which is only
> > useful in hash tables if your index is insufficiently random at the
> > default depth of 3. This does not appear the case, as #'equal itself
> is
> > absent from the profiling report, implying that the hit rate to the
> > index is good.
> >
> > I suppose an 'equal hashtable could keep an 'eq hashtable internally
> for
> > the life of the table. That might be interesting.
> >
> > In any case, I don't want to waste a lot of time reinventing some
> > wheel. If you or any of the other hashtable experts have some wisdom
> > here, I'd be most appreciative.
> >
> > Take care,
> > --
> > Camm Maguire
> c...@maguirefamily.org
> >
> ==========================================================================
> > "The earth is but one country, and mankind its citizens." --
> Baha'u'llah
> >
> >
> > _______________________________________________
> > Gcl-devel mailing list
> > Gcl-devel@gnu.org
> > https://lists.gnu.org/mailman/listinfo/gcl-devel
>
>
>
> --
> Jared C. Davis <ja...@cs.utexas.edu>
> 11410 Windermere Meadows
> Austin, TX 78759
> http://www.cs.utexas.edu/users/jared/
>
>
>
>
>
--
Camm Maguire c...@maguirefamily.org
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
_______________________________________________
Gcl-devel mailing list
Gcl-devel@gnu.org
https://lists.gnu.org/mailman/listinfo/gcl-devel
