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