[isabelle-dev] profiling

[Andreas Schropp]

On 03/01/2010 09:28 PM, Brian Huffman wrote:
> Hello all,
>
> I am trying to use profiling to measure the performance of the HOLCF
> domain package. I recently discovered that I can enable profiling in
> Isabelle with the following command:
>
> ML {* Toplevel.profiling := 1; *}
>
> Here's the output from a "new_domain" command that I tried:
>
> ... (lots of small numbers) ...
>          10 Defs.reduction(4)reduct(3)
>          11 Table().fold_table(1)fold(2)
>          12 Defs.match_args(2)
>          12 Sorts.mg_domain(3)
>          13 Type.raw_match(3)
>          15 List.map(2)
>          16 GARBAGE COLLECTION (update phase)
>          21 GARBAGE COLLECTION (mark phase)
>          39 Table().lookup(2)look(1)
>          39 GARBAGE COLLECTION (total)
>          40 Table().modify(3)modfy(1)
>
> Total: 293; Counted: 293; Uncounted: 0
> ### 1.420s elapsed time, 1.284s cpu time, 0.156s GC time
>
> Apparently the domain package spends a lot of time doing lookups and
> modifications of tables. But I have no idea which functions are
> calling the table library, so this information is basically useless.
>    

Im just guessing from the call dependencies I know:
   it looks like you are doing some overloaded definition which results 
in (quite?) some normalization of the constant dependency tracking in 
defs.ML. But that doesn't explain Sorts.mg_domain - are type-class-heavy 
unifications involved?

> What other profiling tools are available for me to use?

To my knowledge: none.
But you can at least leaverage the existing ones in funny ways, like 
profiling a single function call with profile 1 f x.
And you can profile allocations by replacing 1 by 2, which is much more 
accurate then the monte-carlo-based time profiling.

> It would be
> nice to have something similar to the profiler in GHC, which outputs a
> tree-like table that shows the time spent in each function, as well as
> the total inherited time from all other functions called by it.
>    

Yeah, I loved to have that too.
Performance debugging in Isabelle seems to be mostly guess-and-verify. 
At least thats how I am approaching it.

> - Brian
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>