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 EE07D7EE4B for ; Wed, 16 Oct 2013 17:30:03 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of francois.bobot@cea.fr) identity=pra; client-ip=132.167.192.142; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="francois.bobot@cea.fr"; x-sender="francois.bobot@cea.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of francois.bobot@cea.fr designates 132.167.192.142 as permitted sender) identity=mailfrom; client-ip=132.167.192.142; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="francois.bobot@cea.fr"; x-sender="francois.bobot@cea.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@cirse-out.extra.cea.fr) identity=helo; client-ip=132.167.192.142; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="francois.bobot@cea.fr"; x-sender="postmaster@cirse-out.extra.cea.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvIBANqvXlKEp8COm2dsb2JhbABawyCDAIEdFg4BAQEBAQgJCwkUKIIlAQEFJwsBBUARCxgJFg8JAwIBAgFFEwgCF4drvx+PWBaEDwOePI0wgUA X-IPAS-Result: AvIBANqvXlKEp8COm2dsb2JhbABawyCDAIEdFg4BAQEBAQgJCwkUKIIlAQEFJwsBBUARCxgJFg8JAwIBAgFFEwgCF4drvx+PWBaEDwOePI0wgUA X-IronPort-AV: E=Sophos;i="4.93,508,1378850400"; d="scan'208";a="30596630" Received: from cirse-out.extra.cea.fr ([132.167.192.142]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 16 Oct 2013 17:30:03 +0200 Received: from pisaure.intra.cea.fr (pisaure.intra.cea.fr [132.166.88.21]) by cirse.extra.cea.fr (8.14.2/8.14.2/CEAnet-Internet-out-2.3) with ESMTP id r9GFU34q004215 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT) for ; Wed, 16 Oct 2013 17:30:03 +0200 Received: from muguet2.intra.cea.fr (muguet2.intra.cea.fr [132.166.192.7]) by pisaure.intra.cea.fr (8.14.4/8.14.4) with ESMTP id r9GFU2Jf010121 for ; Wed, 16 Oct 2013 17:30:02 +0200 (envelope-from francois.bobot@cea.fr) Received: from [10.8.32.80] (is222783.intra.cea.fr [10.8.32.80]) by muguet2.intra.cea.fr (8.13.8/8.13.8/CEAnet-Intranet-out-1.2) with ESMTP id r9GFU2fw003213 for ; Wed, 16 Oct 2013 17:30:02 +0200 Message-ID: <525EB0FA.7080302@cea.fr> Date: Wed, 16 Oct 2013 17:30:02 +0200 From: =?ISO-8859-1?Q?Fran=E7ois_Bobot?= User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20131005 Icedove/17.0.9 MIME-Version: 1.0 To: caml-list@inria.fr References: <20131014153023.GA19032@birba.invalid> <525E9CA6.609@ens.fr> <20131016144229.GC17954@birba.invalid> In-Reply-To: <20131016144229.GC17954@birba.invalid> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Marshalling: automatic discard of unmashalable data via ephemerons On 16/10/2013 16:42, Enrico Tassi wrote: > On Wed, Oct 16, 2013 at 04:03:18PM +0200, Jacques-Henri Jourdan wrote: >> The authors of Why3 encountered similar problems. I suggest you to read >> the Weakhtbl module, that gives a solution to this problem. > > Thanks for the hint! > > Indeed they use an imperative list to enqueue/dequeue deletions > that are hence never performed by the finalizer itself. > Another important points is that it allows concurrent access. The finalizer can run when the actual deletions is performed (add can run when iter_remove is run) module ProdConsume : sig type 'a t val create : unit -> 'a t val add : 'a -> 'a t -> unit val iter_remove : ('a -> unit) -> 'a t -> unit end -- François