Profiling F* with OCaml Landmarks

Profiling F* with OCaml Landmarks

This page describes how you can profile FStar using the OCaml Landmarks library (https://github.com/LexiFi/landmarks).

Setup

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)

Automatic profiling

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.

Manual pre-processing based profiling

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.

Manual insertion of landmarks

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.

Things to be aware of

• 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.