[isabelle-dev] Using PolyML's memory consumption profiling on Isabelle

[Makarius]

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.


 	Makarius