From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id E7D927F009 for ; Wed, 25 May 2016 15:20:04 +0200 (CEST) X-IronPort-AV: E=Sophos;i="5.26,364,1459807200"; d="scan'208";a="178977118" Received: from meleze.ens.fr (HELO [129.199.99.114]) ([129.199.99.114]) by mail3-relais-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 25 May 2016 15:20:04 +0200 To: caml-list@inria.fr References: <965631B03C670145ABB9F693E51622530D1279D7@DENBGAT9EK5MSX.ww902.siemens.net> From: Francois Berenger Message-ID: <5745A683.2050108@inria.fr> Date: Wed, 25 May 2016 15:20:03 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Hash consed Patricia trees 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 > > 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 > > > 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"