Hi,
im an Isabelle Developer, wondering about the details of profiling 1&2:
* what happens if another thread is executing while profiling is
active for a selected thread (lets say by calling profile 1 f x in
Isabelle)? In the resulting profile it looks to me like profiling doesnt
know about threads and just accumulates all timings while active. Is
this the same situation for profiling 1 and 2?
* is it possible or even wise to reduce the distance of profiling
1"ticks" to achieve more accurate timings?
* if a call gets "credit" for an allocation in a profiling 2 log, was
the allocation done while profling 2 was active, or did it become
garbage while profling 2 was active?
Regards,
Andy
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
