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
Timing.wrap "mything" (f x y) z
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
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
The timings are automatically presented as a tree which follows the nesting of
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
goblint.timing.json in Perfetto UI.
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 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.
efor expanding/collapsing all callstack levels.
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 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:
perf script -F +pid > OUTPUT_FILE.
- Go to https://profiler.firefox.com/.
- Click "Load a profile from file" and upload
For more information, see Firefox Profiler's documentation.
memtrace is a library and tool for profiling OCaml memory usage.
For a tutorial, see Jane Street Tech Blog.