Profiling¶

FDR provides a tool cspmprofiler that is a time sampling profiler for CSP_M. This means it is possible to attribute how much time is spent in each function within a file whilst checking a refinement assertion, allowing performance problems to be diagnosed.

cspmprofiler can be invoked on the command line by passing it a single CSP_M file:

$ cspmprofiler file.csp

cspmprofiler will evaluate all processes contained in the assertions in the specified file whilst profiling how much time is taken by each function call. Once this has completed, FDR will output a summary of the profiling data, including the total time taken, the total number of allocations performed, a list of the most expensive functions, as well as a hierarchical breakdown of where time and allocations were spent.

For example, suppose cspmprofiler was invoked on Dining Philosophers (i.e. by running cspmprofiler phils6.csp). This would outptu:

Exploring phils6.csp
Exploring SYSTEM :[deadlock free [F]]
Exploring SYSTEMs :[deadlock free [F]]
Exploring BSYSTEM :[deadlock free [F]]
Exploring ASSYSTEM :[deadlock free [F]]
Exploring ASSYSTEMs :[deadlock free [F]]




TOTAL RUNTIME     0.01 secs   (10 ticks @ 1000 us, 1 processor)
TOTAL ALLOCATIONS 10,886,392 bytes  (excludes profiling overheads)


TOP FUNCTIONS

COST CENTRE ENTRIES %time  %alloc
AlphaP      24      100.0  31.6
ASPHILS     1       0.0    0.7
ASPHILSs    1       0.0    0.7
ASSYSTEM    1       0.0    3.3
ASSYSTEMs   1       0.0    3.3
AlphaF      24      0.0    21.1
BSYSTEM     1       0.0    0.7
BUTLER      11      0.0    9.9
FORK        30      0.0    7.9
FORKNAMES   1       0.0    0.0


ALL FUNCTIONS

COST CENTRE ENTRIES  individual         inherited
                    %time  %alloc     %time  %alloc
SYSTEMs     1       0.0    2.0        100.0  34.9
 AlphaP     12      100.0  15.8       100.0  15.8
 AlphaF     12      0.0    10.5       0.0    10.5
 FORK       6       0.0    0.7        0.0    0.7
 PHILs      12      0.0    5.9        0.0    5.9
 union      6       0.0    0.0        0.0    0.0
ASPHILS     1       0.0    0.7        0.0    2.0
 LPHIL      2       0.0    1.3        0.0    1.3
 PHIL       5       0.0    0.0        0.0    0.0
ASPHILSs    1       0.0    0.7        0.0    1.3
 LPHILs     2       0.0    0.7        0.0    0.7
 PHILs      5       0.0    0.0        0.0    0.0
ASSYSTEM    1       0.0    3.3        0.0    3.3
ASSYSTEMs   1       0.0    3.3        0.0    3.3
BSYSTEM     1       0.0    0.7        0.0    10.5
 BUTLER     11      0.0    9.9        0.0    9.9
eats        1       0.0    0.0        0.0    0.0
FORKNAMES   1       0.0    0.0        0.0    0.0
FORKS       1       0.0    0.7        0.0    1.3
 FORK       6       0.0    0.7        0.0    0.7
getsup      1       0.0    0.0        0.0    0.0
N           1       0.0    0.0        0.0    0.0
PHILNAMES   1       0.0    0.0        0.0    0.0
picks       1       0.0    0.0        0.0    0.0
putsdown    1       0.0    0.0        0.0    0.0
sits        1       0.0    0.0        0.0    0.0
SYSTEM      1       0.0    2.0        0.0    43.4
 AlphaF     12      0.0    10.5       0.0    10.5
 AlphaP     12      0.0    15.8       0.0    15.8
 FORK       18      0.0    6.6        0.0    6.6
 PHIL       12      0.0    8.6        0.0    8.6
 union      6       0.0    0.0        0.0    0.0
thinks      1       0.0    0.0        0.0    0.0

We explain the output of each section in turn.

Firstly, the output lists which processes it explored during the profiling. If there were a large number of processes, it would also display its progress. It then outputs a summary of how long it took to explore all the processes, and the total number of bytes allocated during the exploration.

The first import section is the TOP FUNCTIONS section. This is a list of the 10 functions in the script that take the most time overall. In this case, we can see that AlphaP is the most expensive function, in fact taking 100% of the overall execution time. (This example is really too small for profiling to show anything notable.)

The last section displays the time taken by each individual function hierarchically. For example, consider the first few lines

COST CENTRE ENTRIES  individual         inherited
                    %time  %alloc     %time  %alloc
SYSTEMs     1       0.0    2.0        100.0  34.9
 AlphaP     12      100.0  15.8       100.0  15.8
 AlphaF     12      0.0    10.5       0.0    10.5
 FORK       6       0.0    0.7        0.0    0.7
 PHILs      12      0.0    5.9        0.0    5.9
 union      6       0.0    0.0        0.0    0.0

The columns are as follows:

COST CENTRE ENTRIES displays the CSP_M name to which this row refers to.
ENTRIES indicates how many times each entry was called.
individual %time refers to the amount of time was spent in this function. It excludes any time made during calls to other functions.
individual %alloc refers to the number of memory allocations that were made in this function. It excludes any allocations made during calls to other functions.
inherited %time refers to the total amount of time that was spent in this function, including inside any calls to other functions. For example, for SYSTEMs we see that the inherited time is 100%, but the individual time is 0%. This is because the inherited time includes the time inside the recursive call to AlphaP.
inherited %alloc this is similar to inherited %time, but for allocations.

The hierarchy displays which functions are called by which other functions. For example, the above indicates that SYSTEMs calls AlphaP etc. As another example, consider the following profile:

COST CENTRE ENTRIES

f           1
 g          12
  h         12

This indicates that f calls g which calls h.

Note that because cspmprofiler is a sampling profiler, this means that erroneous results can be obtained (although this happens rarely in practice). This is because a sampling profiler periodically records the function at the top of the execution stack. Clearly it is possible that, somehow, the profiler always picks the wrong moment to record this and therefore creates incorrect results.

Internally, cspmprofiler is implemented using the GHC’s profiler for Haskell.