Profiling¶
Timing¶
Timing
is an OCaml module (based on CIL's Stats
) that can be used to profile certain parts of code.
Wrap the function call to be profiled with Timing.wrap
. For example, replace
f x y z
with
Timing.wrap "mything" (f x y) z
where mything
should be replaced with a relevant name to be shown in the output.
Note that all but the last argument are partially applied to f
.
The last argument is given separately for Timing.wrap
to apply and measure.
Then run Goblint with --enable dbg.timing.enabled
or -v
(verbose) to see the timing stats under Timings:
.
The timings are automatically presented as a tree which follows the nesting of Timing.wrap
calls.
Unlike tracing, timings cannot be toggled easily individually, so be considerate of where you leave them after doing the profiling.
Trace Event Format¶
Trace Event Format (TEF) is a simple JSON-based format for profiling data. Besides just accumulating timing information, all timed calls are individually recorded, allowing flamegraph-style visualization.
Goblint can produce a TEF file with
--enable dbg.timing.enabled --set dbg.timing.tef goblint.timing.json
Then open goblint.timing.json
in Perfetto UI.
perf¶
perf
is a Linux profiling tool.
First, record profiling data from a Goblint run:
perf record --call-graph=dwarf ./goblint GOBLINT_ARGUMENTS
Then the resulting perf.data
file can be inspected in various ways.
perf report¶
perf report
is its built-in terminal based viewing tool:
- For top-down hierarchy run:
perf report --children
. - For bottom-up hierarchy run:
perf report --no-children
.
Following keys can be used for navigation:
- Arrows for moving around.
+
for expanding/collapsing one callstack level.e
for expanding/collapsing all callstack levels.q
for quitting.
Function names are mangled: they contain the top-level OCaml module name and function name (or just fun
for lambdas).
Due to inlining some callstack levels might be skipped, making it difficult to follow.
Firefox Profiler¶
Firefox Profiler is a web-based tool, which also supports a form of perf output. It's easier to browse around with and supports additional features like built-in flame graphs.
It can be used as follows:
- Convert
perf.data
by running:perf script -F +pid > OUTPUT_FILE
. - Go to https://profiler.firefox.com/.
- Click "Load a profile from file" and upload
OUTPUT_FILE
.
For more information, see Firefox Profiler's documentation.
Memtrace¶
memtrace
is a library and tool for profiling OCaml memory usage.
For a tutorial, see Jane Street Tech Blog.