Re: [Caml-list] Marshalling: automatic discard of unmashalable data via ephemerons

["François Bobot" <francois.bobot@cea.fr>]

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