Stream: Coq users

Topic: Coq 8.18 slowdown


view this post on Zulip Ralf Jung (Sep 29 2023 at 15:20):

It looks like Coq 8.18 is significantly slower than Coq 8.17, is that expected?
Here's the perf diff for Iris. That's a 6.2% slowdown overall, and a 50% slowdown (!) in the most affected file.

view this post on Zulip Ralf Jung (Sep 29 2023 at 15:22):

(And that's not a small file where small differences look big, it went from 26s to 40s build time.)

view this post on Zulip Ralf Jung (Sep 29 2023 at 15:23):

I'm still gathering data from some projects downstream of Iris.

view this post on Zulip Ralf Jung (Sep 29 2023 at 16:50):

Iron has a .2% overall slowdown, 5% for the worst non-trivial file (details). this can be ignored.

view this post on Zulip Ralf Jung (Sep 29 2023 at 16:51):

our examples have a 1.3% overall slowdown, >40% in the worst file (details). this is real and confirms that the problem isn't just with the core iris lib, but also with projects using Iris.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2023 at 16:55):

@Ralf Jung first thing to look at is differences in OCaml settings / versions between your bench, please post these if you know them.

view this post on Zulip Ralf Jung (Sep 29 2023 at 16:58):

Ill get you the version numbers but they are exactly the same before and after

view this post on Zulip Ralf Jung (Sep 29 2023 at 16:58):

opam shows

ocaml                        4.14.0                    The OCaml compiler (virtual package)
ocaml-config                 2                         OCaml Switch Configuration
ocaml-option-flambda         1                         Set OCaml to be compiled with flambda activated
ocaml-variants               4.14.0+options            Official release of OCaml 4.14.0

(that's for the Iris benchmark)

view this post on Zulip Ralf Jung (Sep 29 2023 at 16:59):

literally the only difference is that we swapped out coq 8.17.0 (or 8.17.1) against 8.18.0

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2023 at 16:59):

I guess first step is trying to see if the regression exists with a non flambda compiler

view this post on Zulip Ralf Jung (Sep 29 2023 at 17:00):

(confirmed its 4.14.0 with flamba everywhere)

view this post on Zulip Ralf Jung (Sep 29 2023 at 17:01):

I'm afraid I'm out of time for investigating this today. I was hoping someone could have some leads. :) it takes quite a while to do these benchmarks and then get the data out.

view this post on Zulip Ralf Jung (Sep 29 2023 at 17:02):

also last time I reported a regression I got told to use flamba. then I spent a day or so getting our entire setup to work with flambda. so its a bit unfair to keep asking us to switch back and forth.^^

view this post on Zulip Ralf Jung (Sep 29 2023 at 17:03):

with my position I dont have that amount of time any more, so all I can do is provide the initial investigation (~30min-1h) and then hope someone can take over / it looks bad enough that someone can make it their priority.

view this post on Zulip Paolo Giarrusso (Sep 29 2023 at 19:30):

It seems Coq MRs should be benchmarked against flambda, shouldn't they?

view this post on Zulip Paolo Giarrusso (Sep 29 2023 at 19:35):

Anyway, can't make promises but I expect we'll be interested at Bedrock at least for our purposes in a few days cc @Janno @Rodolphe Lepigre and @Gregory Malecha

view this post on Zulip Janno (Sep 29 2023 at 20:03):

I'd love to bisect this but I don't actually know how to build external developments with the new dune-based development setup.

view this post on Zulip Janno (Sep 29 2023 at 20:07):

Maybe dune build @install is the right way to go. It seems the resulting coqc binary in _build/install/defaultworks just fine

view this post on Zulip Paolo Giarrusso (Sep 29 2023 at 20:10):

If you need to bisect Coq not Iris, it might help to use a dune build for Iris, I can update my branch. I know Emilio uses this for real in his "Coq universe" but I'm not sure of the details... Dune should be able to build iris before finishing the stdlib build?

view this post on Zulip Janno (Sep 29 2023 at 22:47):

Okay, it seems a bunch of commits that don't actually compile have made it into the git history. So the output of git bisect is not quite as useful as I had hoped:

There are only 'skip'ped commits left to test.
The first bad commit could be any of:
96c1ed00c710dfc2dc233f9cb198ecaebacfe918
b5e989cd9865f1f89014a4a0edafc2fd41fdc719
1d869cee6162c9531afed6b22139f22e88e02d29
605369808c4d033b0111eb889bc92586b2fba65f
0d1c3d0d642ce1c649b6b18f30de5034f56c9564
6fe3d26bf679a27f5c696f43eda35f253d7db7c4
484af13489c9f3c30585e1c4ccf05a96e47136d4
90bae82bb4c82c935cf7b2725255c2d784596df5
a9141c9a8ee427f4d637bc88eb1967463f923b8f

AFAICT the last commit listed there already has the slowdown but I think the order is messed up. Otherwise it would clearly be the first bad commit, wouldn't it? Anyway, it at all seems to point o https://github.com/coq/coq/pull/13448 AFAICT.

view this post on Zulip Janno (Sep 29 2023 at 22:48):

That MR shows >4% slowdown for iris examples and even has some iris developments with individual files that have >50% regression:

   3.2010    5.2430  2.0420  63.79%    87  coq-perennial/src/goose_lang/metatheory.v.html                                                   

view this post on Zulip Paolo Giarrusso (Sep 29 2023 at 22:51):

ah, that MR's benchmarks already claimed 3.8%-4% slowdown and we already had that on the radar

view this post on Zulip Janno (Sep 29 2023 at 22:52):

I must admit I thought it went into 8.17 and didn't have it on my radar anymore

view this post on Zulip Paolo Giarrusso (Sep 29 2023 at 22:53):

FWIW the MR has the correct milestone (while my radar lacked such version info :sweat_smile:).

view this post on Zulip Ralf Jung (Oct 02 2023 at 09:11):

Interestingly, on GPFSL Coq 8.18 is actually a slight speedup. some files get a lot slower but that is overcompensated by other files getting a lot faster.

view this post on Zulip Ralf Jung (Oct 02 2023 at 09:14):

On lambda-rust it's a slight slowdown, again pretty bad on some files

view this post on Zulip Ralf Jung (Oct 02 2023 at 09:14):

lang.v files show up a lot in those files with big slowdowns

view this post on Zulip Janno (Oct 02 2023 at 09:17):

I see a bunch of simplify_eq and simplify_option_eq calls in GPFSL's lang.v. I suppose these call simpl internally?

view this post on Zulip Ralf Jung (Oct 02 2023 at 09:26):

that variants with /= do

view this post on Zulip Ralf Jung (Oct 02 2023 at 10:06):

Emilio Jesús Gallego Arias said:

I guess first step is trying to see if the regression exists with a non flambda compiler

yes it does, 5% total on Iris

view this post on Zulip MackieLoeffel (Nov 30 2023 at 09:15):

I also noticed a significant slowdown in 8.18 in the RefinedC project (up to 50% or more in certain files). It seems that simpl got significantly slower in some cases. As a concrete example, consider the proof of expr_ctx_step_val, adapted the the following:

Lemma expr_ctx_step_val Ki e σ1 κ e2 σ2 ef :
  runtime_step (lang_fill_item Ki e) σ1 κ e2 σ2 ef  is_Some (to_val e).
Proof.
  destruct Ki as [[]|[]?]; inversion 1; simplify_eq.
  all: try (revert select (expr_step _ _ _ _ _ _)).
  all: try (revert select (stmt_step _ _ _ _ _ _ _)).
  all: inversion 1.
  Time all: simpl in *.

On Coq 8.17, the simpl takes 0.05s and on Coq 8.18 it takes around ~0.65s, which is this is a around 13x slower! Is there anything that can be done about this?
(If there is interest, I can see if I can minimize this example.)

view this post on Zulip Pierre Roux (Nov 30 2023 at 09:22):

Might be linked to https://github.com/coq/coq/pull/13448 I think this was already discussed there https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Changes.20to.20simpl.20in.208.2E18.3F (but apparently not about performance).

view this post on Zulip Ralf Jung (Nov 30 2023 at 09:30):

also see the discussion in https://github.com/coq/coq/issues/18168

view this post on Zulip Ralf Jung (Nov 30 2023 at 09:31):

there's a PR on coq master that helps, though things are still slower than they were in 8.17

view this post on Zulip MackieLoeffel (Nov 30 2023 at 09:34):

Thanks for the link to the issue!

view this post on Zulip MackieLoeffel (Nov 30 2023 at 09:36):

What is the PR that you mention? https://github.com/coq/coq/pull/18184 is the only one I see, but it seems to be closed.

view this post on Zulip MackieLoeffel (Nov 30 2023 at 09:46):

Nevermind, I found it: https://github.com/coq/coq/pull/18187 The benches there look quite good, I think this PR probably also resolves the slowdown I am seeing.


Last updated: Jun 22 2024 at 15:01 UTC