Profiling Marabou using perf

To profile Marabou with perf you need:

1. perf - profiling tool (obtained using apt install, run perf to see which package to install)

2. FlameGraph - a perl tool which visualizes perf reports. Tool is available on GitHub - https://github.com/brendangregg/FlameGraph. For more information see here.

3. Ensure debuginfo package is installed on Linux ( this is needed for the DWARF format, which is crucial to obtain correct stack information in the report when working with C/C++).

To profile a Marabou run:

1. Compile Marabou with debug symbols enabled by running cmake .. -DCMAKE_BUILD_TYPE=Debug. It might be a good idea to turn off Marabou logging for this to avoid needless IO operations.

2. Executing perf record -g dwarf ./Marabou ... will sample performance information into perf.data file. Longer runs can accumulate considerable amounts of data. To specify a smaller sampling rate in Hz use -F samplingRate (default value is 99).

3. Executing perf report shows a report with the function calls sorted by fraction of total runtime. While this is readable, it can be challenging to understand when a call occurs, especially if the same method is used in multiple contexts.

4. To generate a FlameGraph of the report use the piped command: perf script | stackcollapse-perf.pl | flamegraph.pl > filename.svg (assuming the scripts in FlameGraph folder are added to the PATH)

5. A FlameGraph represents nested function calls / stack trace along the Y axis, and the duration of each call along the X axis. So the nested method calls appear on top of each other, while their width represents time allocation of each call. The ?? boxes in the plot represent in-lined functions and can be ignored (you should double check that they are consistent with the -stdio report version of the data).