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

[David Matthews]

On 14/10/2011 10:56, Makarius wrote:
> On Fri, 14 Oct 2011, Andreas Schropp wrote:
>> val dummy_task = Task(NONE, ~1)
>>
>> Values are not shared?! What the hell?

Datatypes and tuples that contain only constant data are created once 
during compilation.

> This looks like an older version. Thomas was referring to this one in
> Isabelle/73dde8006820:
>
> fun dummy_task () =
> Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing =
> new_timing ()};
>
> Since the timing is a mutable variable here, it has to be created afresh
> for each use -- in Future.value construction. Normally 1 million extra
> allocations are not a big deal, but an experiment from yesterday shows
> that there is in fact a measurable impact. See now Isabelle/2afb928c71ca
> and the corresponding charts at
> http://www4.in.tum.de/~wenzelm/test/stats/at-poly.html
>
> 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?

Regards,
David