Andreas Schropp wrote:

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?

If profiling is turned on it is turned on for all threads.

Profiling 2 records the number of words allocated in each function. It works by pretending that the heap segment is full for each allocation so forcing a call into the RTS. This adds a considerable overhead but does produce accurate figures rather than samples. It measures the allocation made and takes no account of whether or when the data structures are garbage collected.

Profiling 1 samples the program counter to find out where the code is spending most of its time. It only really works properly in Linux. Mac OS X does not have thread-specific CPU timers. In Linux a timer is set for each thread which causes it to be interrupted every millisecond of CPU time. One millisecond seems like a reasonable figure but you could try changing it. You would have to modify Processes::StartProfilingTimer in the RTS.

Regards, David