Skip to content

Profiling F* with Spacetime

Jump to bottom Edit New page
Tom Kelly edited this page Aug 12, 2019 · 2 revisions

Profiling F* with Spacetime

The OCaml Spacetime profiler allows you to see where in your program memory is allocated.

Setup an opam switch with Spacetime and all your opam packages:

 $ opam switch export opam_existing_universe
 $ opam switch create 4.07.1+spacetime
 $ opam switch import opam_existing_universe

NB: you might have a stack size issue with the universe, you can expand it to 128M in bash with ulimit -S -s 131072.

In the 4.07.1+spacetime switch, build fstar. This will take some time.

Now run fstar, using the environment variable OCAML_SPACETIME_INTERVAL to turn on profiling and specify how frequently Spacetime should inspect the OCaml heap (in milliseconds):

 $ OCAML_SPACETIME_INTERVAL=100 program-to-run program-arguments

e.g.

OCAML_SPACETIME_INTERVAL=100 bin/fstar.exe --admit_smt_queries true --warn_error -271 --z3cliopt 'timeout=600000' --use_hints --use_extracted_interfaces true examples/micro-benchmarks/Unit1.Parser.fst

This will output a file of the form spacetime-<pid>.

To view the information in this file, we need to process it with prof_spacetime. Right now, this only runs on OCaml 4.06.1 and lower. Install as follows:

 $ opam switch 4.06.1
 $ opam install prof_spacetime

To post-process the results do

 $ prof_spacetime process -e bin/fstar.exe spacetime-<pid>

This will produce a spacetime-<pid>.p file.

To serve this and interact through a web-browser do:

 $ prof_spacetime serve -p spacetime-<pid>.p

To look at the data through a CLI interface do:

 $ prof_spacetime view -p spacetime-<pid>.p

For more on Spacetime and its output see:

Add a custom footer
Add a custom sidebar
Clone this wiki locally