[findlib] Performance issue with large opam switches

[ejgallego]

It seems plugin instrumentation is taking a large tool on large opam switches, likely due to findlib being slow on them.

This makes file startup quite slow on my system at some point. For reference, times for fcc simple.v:

• minimal switch: 0.2 secs
• plus memtrace_viewer: 5.88 secs

There is a super-linear overhead somewhere.

[SkySkimmer]

simple.v = https://github.com/ejgallego/coq-lsp/blob/main/examples/rewrite/simple.v ?

[ejgallego]

simple.v: any file that uses the prelude, for example Definition a := 3.

Numbers before installing memtrace_viewer:

Fl_dynload.load_packages: coq-lsp.serlib.ltac , 0.028070 ms
Fl_dynload.load_packages: coq-lsp.serlib.number_string_notation , 0.025253 ms
Fl_dynload.load_packages: coq-lsp.serlib.tauto , 0.025031 ms
Fl_dynload.load_packages: coq-lsp.serlib.cc_core , 0.025120 ms
Fl_dynload.load_packages: coq-lsp.serlib.cc , 0.024681 ms
Fl_dynload.load_packages: coq-lsp.serlib.firstorder_core , 0.025205 ms
Fl_dynload.load_packages: coq-lsp.serlib.firstorder , 0.025410 ms

Numbers after:

Fl_dynload.load_packages: coq-lsp.serlib.ltac , 0.554432 ms
Fl_dynload.load_packages: coq-lsp.serlib.number_string_notation , 0.567631 ms
Fl_dynload.load_packages: coq-lsp.serlib.tauto , 0.547607 ms
Fl_dynload.load_packages: coq-lsp.serlib.cc_core , 0.550585 ms
Fl_dynload.load_packages: coq-lsp.serlib.cc , 0.549075 ms
Fl_dynload.load_packages: coq-lsp.serlib.firstorder_core , 0.583141 ms
Fl_dynload.load_packages: coq-lsp.serlib.firstorder , 0.558694 ms

@SkySkimmer Rocq upstream could be affected, do you mind checking?

[ejgallego]

I'm not sure Rocq would be affected as we don't directly use Fl_dynload, but indeed, this problem is independent of coq-lsp:

Fl_dynload.load_packages: rocq-runtime.plugins.ltac , 0.364408 ms
Fl_dynload.load_packages: rocq-runtime.plugins.number_string_notation , 0.371798 ms
Fl_dynload.load_packages: rocq-runtime.plugins.tauto , 0.366933 ms
Fl_dynload.load_packages: rocq-runtime.plugins.cc_core , 0.377898 ms
Fl_dynload.load_packages: rocq-runtime.plugins.cc , 0.383520 ms
Fl_dynload.load_packages: rocq-runtime.plugins.firstorder_core , 0.369068 ms
Fl_dynload.load_packages: rocq-runtime.plugins.firstorder , 0.369629 ms

[ejgallego]

The function that takes the large runtime is Fl_package_base.requires_deeply , Rocq callsFindlib.package_deep_ancestors in Mltop.add_deps which is basically an alias to this function.

However this function is only called when compiling files that have a Declare Ml Module on them, so the impact is very low in most situations.

It could however affect plugin writers, as if they have a very large switch, then the .vo file compilation would take in excess of dozens of seconds.

[ppedrot]

FWIW I tried to execute a few randomly sampled Declare ML Module with rocq and I don't see any trace of findlib appearing in the profile. It does through fcc though, since I have a rather big opam switch.

[ejgallego]

@ppedrot do your examples trigger Mltop.add_deps ?

This is where the call to Findlib.package_deep_ancestors happens.

Note that fcc does several calls to load the serlib plugins, so usually have the overhead 7x due to the number of calls, so it is more noticeable.

[SkySkimmer]

From a basic opam switc, after for i in $(seq 1 2000); do mkdir -p /tmp/wk/foo$i && touch /tmp/wk/foo$i/META; done:

• running env OCAMLPATH="/tmp/wk:$OCAMLPATH" rocq c foo.v and rocq c foo.v with foo.v a trivial file both take about 0.1s
• fcc with base OCAMLPATH takes about 0.2s
• fcc with extended OCAMLPATH takes about 1.8s

After installing memtrace_viewer:

• rocq c still around 0.1s (lots of variance, I can see 0.05s and rarely 0.2s as well)
• rocq c with /tmp/wk in OCAMLPATH still around 0.1s (lows are more 0.06s than 0.05s but not sure that's meaningful)
• fcc around 1.9s
• fcc with /tmp/wk in OCAMLPATH around 4s

The basic switch has about 50 subdirs of lib/, after installing memtrace_viewer around 180, so it seems the content of the META matters (180 << 2000 but has about the same impact)? Or possibly time is spent in string comparisons which go faster with the uniform fooXXX I generated? IDK

[SkySkimmer]

BTW this is what we get with

Set Debug "dynlink".
Declare ML Module "coq-lsp.serlib.ltac".

:

  for coq-lsp.serlib.ltac:
  all deps:
    unix
    threads.posix
    threads
    base.base_internalhash_types
    base.caml
    base.shadow_stdlib
    sexplib0
    base
    ppx_compare.runtime-lib
    ppx_deriving.runtime
    ppx_deriving_yojson.runtime
    ppx_sexp_conv.runtime-lib
    ppx_hash.runtime-lib
    findlib.internal
    findlib
    dynlink
    findlib.dynload
    memprof-limits
    str
    rocq-runtime.clib
    rocq-runtime.config
    rocq-runtime.boot
    rocq-runtime.perf
    rocq-runtime.lib
    rocq-runtime.gramlib
    rocq-runtime.vm
    rocq-runtime.kernel
    rocq-runtime.library
    rocq-runtime.engine
    rocq-runtime.pretyping
    zarith
    rocq-runtime.interp
    rocq-runtime.parsing
    rocq-runtime.proofs
    rocq-runtime.printing
    rocq-runtime.tactics
    rocq-runtime.vernac
    bigarray
    parsexp
    sexplib
    seq
    yojson
    coq-lsp.serlib
    rocq-runtime.plugins.ltac
    coq-lsp.serlib.ltac
  filtered deps:
    base.base_internalhash_types
    base.caml
    base.shadow_stdlib
    sexplib0
    base
    ppx_compare.runtime-lib
    ppx_deriving.runtime
    ppx_deriving_yojson.runtime
    ppx_sexp_conv.runtime-lib
    ppx_hash.runtime-lib
    bigarray
    parsexp
    sexplib
    seq
    yojson
    coq-lsp.serlib
    coq-lsp.serlib.ltac

"all deps" is the result of package_deep_ancestors, "filtered deps" removes non explicit already loaded packages.

(debug print code at https://github.com/rocq-prover/rocq/blob/501ef8dd60d92fed5209c6e4a42a8065de9cd097/vernac/mltop.ml#L199, slightly modified formatting from rocq-prover/rocq#20701)

[ejgallego]

@SkySkimmer I think the algorithm in Findlib.package_deep_ancestors may be quadratic, but I need to look more into it.

It could also be some other problems with findlib and the way we use it (we do a hack to reinit, etc...)