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

[David Matthews]

On 14/10/2011 09:13, Andreas Schropp wrote:
> 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?)

Profiling 3 is the number of cases where the run-time system had to 
emulate an arithmetic operation because the operation required 
long-precision arithmetic.  This is a LOT more expensive than doing the 
arithmetic with short precision ints so it may be worth recoding 
hot-spots that show up with this.

Profiling 4 has just been added so it probably has teething-troubles.

I would really prefer to replace these numbers by a datatype so that 
users don't have to remember numbers.

Regards,
David