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

[Andreas Schropp]

On 10/13/2011 01:24 PM, Thomas Sewell wrote:
> Good day all. Just wanted to let the Isabelle developers know about the latest feature David Matthews has added to PolyML, and to let you all know how useful it is.
>
> The feature allows profiling of objects after garbage collection. When code is compiled with PolyML.compiler.allocationProfiling set to 1, all objects allocated are also given a pointer to their allocating function. When the garbage collector runs with PolyML.compiler.profiling set to 4, a statistical trace is printed of which objects survived garbage collection.
>    

Cool.

So we have:
   profiling = 1 approximates runtime Monte-Carlo style sampling of the 
program counter
   profiling = 2 records the number of words allocated in each function 
(very accurate IIRC)
   profiling = 3 ???
   profiling = 4 counts GC survivors (very accurately?)


> This means that for Isabelle we get our first real look at what is taking up space at runtime and in images.
>
> I include the last 20 lines of traces produced at four interesting points
>    1) After including the HOL theories in HOL's ROOT.ML
>    2) After performing a PolyML.shareCommonData after (1)
>    3) After adding a 400-element record to a test theory built on the HOL image.
>    4) After performing a shareCommonData after (3)
>    

These are traces for profiling=4?

> Isabelle is generating a *lot* of copies of types&  terms, particularly via
> Term.map_atyps. Since shareCommonData eliminates them, many are
> duplicates. It's possible that further use of the "same" variants from
> Term_Subst might help. It's also possible that the repeated reconstruction is
> necessary (e.g. repeated generalization/abstraction of type variables) and
> further use of the new Term_Sharing mechanism might be the answer.
>    

The way I learned Isabelle programming one views term-traversal as being 
cheap,
which seems to be true most of the time especially when they are freshly 
allocated
with nice locality properties. Sharing lots of subterms might interfere 
with this.
Isn't this what GC was made for? Why introduce artificial sharing?

BTW: the Coq kernel does huge amounts of sharing IIRC.
Should we be concerned or is this just a thing because of proof terms?

Makarius, please comment on this, because now I feel like a wasteful
programmer. ;D


> A large quantity of the persistent objects are Table and Net objects, as
> expected.
>
> There are surprisingly many dummy tasks.
>    

What is a dummy task?

> A surprisingly large quantity of the persistent objects are associated with
> proof terms and name derivations. This is presumably not Thm.name_derivation
> but inlined code from its subcalls Proofterm.thm_proof, proof_combP,
> proof_combt' and Library.foldl, none of which are listed. If indeed these foldl
> loops are producing this many objects then perhaps the work done unconditionally
> here should be rethought.
>    

For proofs=0?
Taking a guess these might be the PBody thms pointers.

Cheers,
   Andy