Profiling F* with Linux perf

Profiling F* with Linux perf

perf is a statistical profiler on Linux that can profile a binary without needing instrumentation.

To profile fstar with perf try:

 $ perf record --call-graph dwarf -i -e cycles:u -- <program-to-run> <program-arguments> 
 $ # for example you can profile the Mac.fst micro-benchmark with
 $ perf record --call-graph dwarf -i -e cycles:u -- bin/fstar.exe --admit_smt_queries true \
   --warn_error -271 --use_hints --use_extracted_interfaces true examples/micro-benchmarks/Mac.fst

Viewing your results:

• This will give you a list of hotspots in your program where the sample was in that function

perf report --no-children

• This will give you a list of child inclusive call-chains in your program

perf report --children

There is help within the perf report which can be got by pressing ? There is more help with perf report --help

If perf can find the source code, it can do a better job of annotating your report. If you use opam to manage your OCaml libraries, the following will keep all the source files from the build in the current switch:

opam switch reinstall --keep-build-dir

To allow non-root users to use perf on Linux, you may need to execute:

 $ echo 0 | sudo tee /proc/sys/kernel/perf_event_paranoid

Further links:

• Linux perf wiki: https://perf.wiki.kernel.org/index.php/Main_Page
• Brendan Gregg's perf notes: http://www.brendangregg.com/perf.html