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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
