-
Notifications
You must be signed in to change notification settings - Fork 235
Profiling F* with OCaml Landmarks
This page describes how you can profile FStar using the OCaml Landmarks library (https://github.com/LexiFi/landmarks).
You need to install landmarks into the opam switch you are using to build FStar, this can be done with:
opam install landmarks
You will need to add the following to your FStar _tags
file:
true:
package(landmarks), package(landmarks.ppx)
To use the landmarks automatic pre-processing instrumentation to profile specific FStar modules you need to:
- Add the preprocessing command to the modules of interest in ocamlbuild
_tags
. For example:
<src/ocaml-output/FStar_{TypeChecker_Normalize,TypeChecker_Tc,TypeChecker_Util,Universal}.ml>: \
ppx(`ocamlfind query landmarks.ppx`/ppx.exe --as-ppx --auto)
- Rebuild the FStar compiler:
make -C src rebuild
- Run a file with the landmarks configured on. For example:
OCAML_LANDMARKS='on,output=landmarks.out' bin/fstar.exe --admit_smt_queries true --z3cliopt 'timeout=600000' --smtencoding.valid_intro true --smtencoding.valid_elim true --use_hints --use_extracted_interfaces true examples/micro-benchmarks/Mac.fst
The callgraph output will be in the landmarks.out
file.
With landmarks you can manually insert pre-processing commands to instrument specific functions in the OCaml extracted sources:
let[@landmark] f = body
You need to make sure that the landmarks pre-processor is enabled for the FStar module that you have added your landmarks to.
You can bind the landmarks to FStar by adding the following to src/basic/boot/FStar.Util.fsi
:
type lm_t
val register_lm: string -> lm_t
val enter_lm: lm_t -> unit
val exit_lm: lm_t -> unit
and this to src/basic/ml/FStar_Util.ml
:
type lm_t = Landmark.landmark
let register_lm name = Landmark.register name
let enter_lm name = Landmark.enter name
let exit_lm name = Landmark.exit name
This will allow you to define landmarks from FStar by registering your landmarks at top-level and then using them. For example:
let my_fn_to_profile_lm = Util.register_lm "my_fn_to_profile"
let my_fn_to_profile x y =
...
Util.enter_lm batch_mode_tc_lm;
... <something we want to measure>
Util.exit_lm batch_mode_tc_lm;
...
You need to be careful to ensure that exit_lm
is called even in the presence of exceptions.
- The timing and allocation information is inclusive of all the landmarks contained within a landmark enter/exit pair. This means that the timing and allocation data can include the overhead of the landmark library.
- Inserting the landmark profiling points can change the behaviour of the inlining optimizations done by the compiler.
- There can be a limit to how many landmarks can be collected. When running with all files in
src/ocaml-output/*.ml
set to auto instrument, the library could stack overflow. It is also unclear if the timing information is reflective of reality once every function call has instrumentation overhead.