Hi,

The Value Analysis plugin of Frama-C uses hash-consing of Patricial trees
extensively. In fact, some analyses would not run without it at all. See
Section 9 of cristal.inria.fr/~doligez/publications/cuoq-doligez-mlw-2008.ps
for more details. Unfortunately, as mentioned there, no figures exist for
with hash-consing vs. without hash-consing -- but most of the examples
would have failed without it.

Although I'm not sure what was implemented exactly at the time, one
important feature when using hash-consed Patricia trees is the possibility
of using caches. Alain mentioned this in this mail:

> Also, you get a nice unique integer for each tree. This allow you to
> memoize efficiently set operations (like union, intersection, for which
> you can use memoization in the inner loop, not only at toplevel), and to
> build sets of sets (and so on).

I should stress that the possibility of memoizing *in the inner loop*, is
crucial. When performing e.g. unions or map2 operations, it is possible to
return a result in constant time when either
- the two trees is equivalent (because e.g. union s s == s)
- the two trees have already been merged, and the result is in the cache.
In practice, most operations become O(D ln D), where D is the number of
differences between the two trees, or even O(1) if the cache is big enough
and the operations repetitive enough.

If this kind of caching may be useful to you, the files hptmap*.ml* of
Frama-C provides very nice iterators and abstractions.

HTH,


On Mon, May 23, 2016 at 4:33 PM, Neuhaeusser, Martin <
martin.neuhaeusser@siemens.com> wrote:

> Dear all,
>
> during some experiments with integer set implementations, I came across a
> discussion on that list that proposed to use Patricia trees and hash
> consing on the tree nodes' constructors to achieve maximal sharing:
>
> http://caml.inria.fr/pub/ml-archives/caml-list/2008/03/5be97d51e2e8aab16b9e7e369a5a5533.en.html
>
> Is anyone aware of a corresponding implementation that also has a
> performance benefit (or, at least, no negative performance impact) compared
> to standard sets or to non-hash consed Patricia trees? Or is anyone aware
> of a paper on that matter?
>
> Sadly, in all my experiments, the combination of Patricia trees with hash
> consing applied to the terms representing the tree has a horrible impact on
> performance (a slowdown by an order of magnitude). After spending some
> thoughts, this seems to be reasonable given the structure of a Patricia
> tree. In particular, we found no way to make significand use of the
> reflexivity properties obtained by hash consing in set operations like
> subset or union. In our benchmarks, the time for constructing hash-consed
> subtrees during set operations outweighs any gains obtained by the
> "physical equality = set equality" property. Or is the whole point in the
> earlier discussion the possibility to use hash consing tags for memoization
> of set operations?
>
> Any hints and comments are highly appreciated. It would really be great if
> some of the participants from the 2008 discussion could perhaps share their
> experience.
>
> Best regards,
> Martin
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs




-- 
Boris