Stream: Coq devs & plugin devs

Topic: Missed inlining optimization


view this post on Zulip Guillaume Melquiond (Nov 24 2022 at 06:17):

I was looking at the assembly code of Parray.set. Indeed, this function computes Uint63.le Uint63.zero n, which is true by definition. So, I was wondering if the OCaml compiler was able to optimize it away, or if we should just help the compiler by removing it. To my great surprise, not only is it not optimized, but the call to Uint63.le is not even inlined. In fact, it is worth than that; it is not even a direct call, it is a full-blown closure invocation through caml_apply2. So, what should have been a noop is actually a bitcoin-grade waste of computing resources.

view this post on Zulip Guillaume Melquiond (Nov 24 2022 at 06:18):

For the record, here is Uint63.le:

let le (x : int) (y : int) =
  (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000)
[@@ocaml.inline always]

So, are we using the attribute wrong? Or is it a bug in the OCaml compiler? Or is it a feature of Dune?

view this post on Zulip Maxime Dénès (Nov 24 2022 at 08:29):

Ouch!

view this post on Zulip Guillaume Melquiond (Nov 24 2022 at 08:37):

$ dune build _build/install/default/bin/coqtop.opt
File "kernel/parray.ml", line 122, characters 5-47:
122 |   if (Uint63.le [@ocaml.inlined]) Uint63.zero n && Uint63.lt n l then
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error (warning 55 [inlining-impossible]): Cannot inline: Unknown function

view this post on Zulip Maxime Dénès (Nov 24 2022 at 08:38):

Unknown function?

view this post on Zulip Maxime Dénès (Nov 24 2022 at 08:38):

Do we pass -opaque or whatever it's called?

view this post on Zulip Maxime Dénès (Nov 24 2022 at 08:39):

Do you get the same thing if you build in "release" mode?

view this post on Zulip Guillaume Melquiond (Nov 24 2022 at 08:44):

Indeed, it works in release mode.

view this post on Zulip Guillaume Melquiond (Nov 24 2022 at 08:44):

But then, it begs the question, when we are doing benchs, are we doing them in release mode?

view this post on Zulip Pierre Roux (Nov 24 2022 at 08:49):

If benchs are based on the OPAM packages (coq-core.opam), those are built in release mode.

view this post on Zulip Guillaume Melquiond (Nov 24 2022 at 08:51):

Where is the --profile=release option passed?

view this post on Zulip Gaëtan Gilbert (Nov 24 2022 at 08:53):

dune build -p implies release IIRC

view this post on Zulip Gaëtan Gilbert (Nov 24 2022 at 08:54):

       -p PACKAGES, --for-release-of-packages=PACKAGES (required)
           Shorthand for --release --only-packages PACKAGE.

from man dune build

view this post on Zulip Gaëtan Gilbert (Nov 24 2022 at 08:54):

and

       --release
           Put dune into a reproducible release mode. This is in fact a
           shorthand for --root . --ignore-promoted-rules --no-config
           --profile release --always-show-command-line
           --promote-install-files --default-target @install
           --require-dune-project-file.

Last updated: May 31 2023 at 15:01 UTC