[isabelle-dev] Using PolyML's memory consumption profiling on Isabelle
makarius at sketis.net
Fri Oct 14 13:31:21 CEST 2011
On Fri, 14 Oct 2011, David Matthews wrote:
>> I can only guess that allocation of mutable stuff costs extra.
> Allocation of a mutable, at least a fixed-size mutable such as ref,
> doesn't cost any more than allocating an immutable. However, if a
> mutable survives a GC it has an impact on subsequent GCs. The worst
> case would be a mutable that survived one GC and then becomes
> unreachable. It would continue to be scanned in every partial GC until
> it was thrown away by the next full GC. Does this correspond with what
> you've found?
Yes, I was thinking in terms of the survival of the mutable, not the
initial allocation. What happened in the example is that any Future.value
(which is conceptually immutable) would retain a mutable field for timing
information that is reachable but semantically never used later on.
Thus it somehow impacts later memory management indirectly, leading to the
measurable (but very small) overhead.
More information about the isabelle-dev