Re: [Caml-list] Hash consed Patricia trees

[Francois Berenger <francois.berenger@inria.fr>]

On 25/05/2016 14:29, Boris Yakobowski wrote:
> 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
> <http://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.

It might even be useful to have this data structure in opam provided as 
a standalone library.

> HTH,
>
>
> On Mon, May 23, 2016 at 4:33 PM, Neuhaeusser, Martin
> <martin.neuhaeusser@siemens.com <mailto: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

-- 
Regards,
Francois.
"When in doubt, use more types"