Does flambda slow down Coq?

Using Coq
1

If I want coq to be fast, should I use flambda today? In my very quick and unscientific try, the resulting Coq 8.10.0 seems ~20% slower! There could be a million reasons or mistakes on my part, or my coq code might be odd, so please ignore that result, but I have questions.

I’d like to reproduce, at some point, some benchmarks where coq does get faster with flambda. Yet I found none!
Does anybody have experience? You can ignore coq’s install time, only consider coqc time.

I did find https://coq-bench.github.io/ and https://github.com/coq/coq-bench.

(I have some more details on https://twitter.com/Blaisorblade/status/1186470962948165633 on what I did, but it’s absolutely not worth examining).
EDIT: this was with 4.09.

1 Like
2

flambda is faster except when compiling native compute stuff
Coq’s stdlib precompiles native compute stuff so it’s slower unless you configure -native-compute no or use dune (which doesn’t support native compute yet)
For instance see https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/631/console


┌────────────────────────┬──────────────────────────┬─────────────────────────────────────────────┬──────────────────────────────────────────────┬───────────────────────────────┬────────────────────────────┐
│                        │      user time [s]       │                 CPU cycles                  │               CPU instructions               │     max resident mem [KB]     │         mem faults         │
│                        │                          │                                             │                                              │                               │                            │
│           package_name │     NEW     OLD  PDIFF   │              NEW               OLD  PDIFF   │               NEW               OLD  PDIFF   │        NEW        OLD PDIFF   │     NEW     OLD    PDIFF   │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│            coq-unimath │ 1680.90 1951.25 -13.86 % │    4658867417753     5411393914037 -13.91 % │     8065896438035     9432775235370 -14.49 % │     992956    1007012 -1.40 % │     856     156  +448.72 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│        coq-lambda-rust │ 1795.24 2077.30 -13.58 % │    4998648300508     5784968113043 -13.59 % │     6723256819689     7979796059985 -15.75 % │    1487280    1421348 +4.64 % │      57       0     +nan % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│             coq-geocoq │ 1755.28 2027.31 -13.42 % │    4871402558021     5629282210567 -13.46 % │     7009624771817     8143644223348 -13.93 % │    1327780    1229176 +8.02 % │     549     216  +154.17 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│ coq-mathcomp-character │  220.76  252.06 -12.42 % │     615177207070      701953393575 -12.36 % │      837097782503      969030635197 -13.61 % │    1099520    1066568 +3.09 % │       0       4  -100.00 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│        coq-fiat-crypto │ 3402.38 3881.53 -12.34 % │    9435236895129    10763749140824 -12.34 % │    14501728948829    16956120995559 -14.47 % │    2528272    2492708 +1.43 % │    3168    1406  +125.32 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│ coq-mathcomp-odd-order │ 1214.01 1384.61 -12.32 % │    3381637316792     3857163743265 -12.33 % │     5551557711625     6409068514419 -13.38 % │    1376128    1372848 +0.24 % │       1       6   -83.33 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│     coq-mathcomp-field │  194.11  221.33 -12.30 % │     539554541614      615402552024 -12.32 % │      775634251088      895000758063 -13.34 % │     793496     760476 +4.34 % │      28       0     +nan % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│               coq-hott │  296.29  336.22 -11.88 % │     810361671537      923596468176 -12.26 % │     1209851309365     1403579748573 -13.80 % │     510060     479236 +6.43 % │     782       1 +78100.00 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│  coq-mathcomp-solvable │  169.61  192.07 -11.69 % │     471388187405      534104564775 -11.74 % │      617904876673      716806822797 -13.80 % │     907876     850552 +6.74 % │     174       2 +8600.00 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│            coq-bignums │   64.45   72.44 -11.03 % │     178000539580      199552768548 -10.80 % │      230579968246      260500281822 -11.49 % │     558700     545496 +2.42 % │     396       0     +nan % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│                coq-vst │ 2885.66 3228.61 -10.62 % │    8024000627885     8980450021200 -10.65 % │    10771126565796    12448577870728 -13.48 % │    2159588    2225308 -2.95 % │     369     586   -37.03 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│   coq-mathcomp-algebra │  139.65  156.00 -10.48 % │     388079747067      433693706039 -10.52 % │      477583335429      549233820833 -13.05 % │     687300     658520 +4.37 % │     204      24  +750.00 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│  coq-mathcomp-fingroup │   49.34   55.09 -10.44 % │     137195128738      152883706072 -10.26 % │      175428536706      199952759548 -12.27 % │     631556     594020 +6.32 % │       1     209   -99.52 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│               coq-corn │ 1373.18 1529.18 -10.20 % │    3809388654755     4242939008044 -10.22 % │     5472730208259     6204322448994 -11.79 % │     849200     875512 -3.01 % │      77      46   +67.39 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│       coq-math-classes │  208.50  227.43  -8.32 % │     573766057000      625695780404  -8.30 % │      688643614869      788941646755 -12.71 % │     572596     531404 +7.75 % │     104      85   +22.35 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│           coq-compcert │  820.96  885.77  -7.32 % │    2274065840301     2455000878636  -7.37 % │     3177978783162     3507251859788  -9.39 % │    1406928    1313960 +7.08 % │     455     185  +145.95 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│              coq-flocq │  529.46  566.07  -6.47 % │    1470967833006     1575628090854  -6.64 % │     2080296252831     2284763219058  -8.95 % │    1640488    1784692 -8.08 % │     349     386    -9.59 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│              coq-color │  676.86  722.88  -6.37 % │    1874108918639     2003618805292  -6.46 % │     2147566570236     2383608651270  -9.90 % │    1482932    1443248 +2.75 % │     293     115  +154.78 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│       coq-fiat-parsers │  673.06  714.53  -5.80 % │    1866230357432     1982290856398  -5.85 % │     2740465494134     2986017208609  -8.22 % │    3052992    2926592 +4.32 % │     620     887   -30.10 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│ coq-mathcomp-ssreflect │   38.23   40.04  -4.52 % │     104344887457      109593537080  -4.79 % │      121772880607      130998264156  -7.04 % │     580516     539472 +7.61 % │      36      53   -32.08 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│             coq-sf-plf │   44.79   46.41  -3.49 % │     123140235733      127068497608  -3.09 % │      151928738601      160526552228  -5.36 % │     563028     521420 +7.98 % │     212       0     +nan % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│    coq-formal-topology │   31.02   32.08  -3.30 % │      82889829092       85172035455  -2.68 % │      104758782104      111274145229  -5.86 % │     525788     485124 +8.38 % │      21       0     +nan % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│         coq-coquelicot │   76.60   78.18  -2.02 % │     209564568583      213940551750  -2.05 % │      241437769650      255896240519  -5.65 % │     761832     712192 +6.97 % │     340      15 +2166.67 % │
├────────────────────────┼──────────────────────────┼─────────────────────────────────────────────┼──────────────────────────────────────────────┼───────────────────────────────┼────────────────────────────┤
│          coq-fiat-core │  117.70  112.99  +4.17 % │     326328799581      312535973990  +4.41 % │      393000898939      388867556448  +1.06 % │     545392     507756 +7.41 % │     606     182  +232.97 % │
└────────────────────────┴──────────────────────────┴─────────────────────────────────────────────┴──────────────────────────────────────────────┴───────────────────────────────┴────────────────────────────┘
1 Like
3

Cool thanks, I’m gonna try reproducing that and isolate the difference… first, I’m installing 4.07.1+flambda+no-flat-float-array and 4.07.1.

4

So the problem is still there with those compilers on Mac with make -j4, for both coq-stdpp.dev.2019-09-19.1.9041e6d8. Similarly, flambda gives a ~13% slowdown on coq-bignums (75s vs 85s). Mistakes are still possible, but I’ve ruled out the most obvious ones. Next, I should try rerunning my scripts on Linux, to see if the platform makes any difference.

On my 4-core 8-thread MacBookPro (Intel Core i7 3,1GHz, 16GB RAM, macOS 10.14.6), flambda appears slower than vanilla on coq.8.10.0 compiling coq-stdpp.dev.2019-09-19.1.9041e6d8, which does not use native-compute AFAIK (and comes from many of the same authors as lambda-rust).

More data on this for stdpp here.

Here are results for coq-bignums. These ones are with Turbo Boost disabled.

$ grep user *.log|awk '{print $1, $4, $5}'
coq-bignums-8.10.0-bench-ocaml407-coq-8.10.0.log: 75.25 user
coq-bignums-8.10.0-bench-ocaml407-coq-8.10.0.log: 75.40 user
coq-bignums-8.10.0-bench-ocaml407-coq-8.10.0.log: 75.47 user
coq-bignums-8.10.0-bench-ocaml407-flambda-coq-8.10.0.log: 85.63 user
coq-bignums-8.10.0-bench-ocaml407-flambda-coq-8.10.0.log: 85.43 user
coq-bignums-8.10.0-bench-ocaml407-flambda-coq-8.10.0.log: 86.05 user

EDIT: my homegrown benchmark harness is in https://github.com/Blaisorblade/my-ocaml-coq-benchs — once again, it’s nowhere near good, but it’ll do the job here.

5

In order to get some speedup you need to be sure the right -flambda specific options are passed down to Coq configure’s. For example OPAM packages don’t do that.

Also newer OCaml or Coq versions could interfere badly, but yes, in the past flambda provided a speedup on the lines Gaëtan pointed out.

1 Like
6

This is what I see on my macbook (for stdpp, make -j1): coq+flambda.org · GitHub

1 Like
7

Thanks @leif! I get similar results even with 4.07 — so -native-compute no is needed to actually get a speedup. Moreover, that option by itself isn’t responsible for the speedup.

https://github.com/coq/coq/pull/10975 proposes changing docs accordingly.

However, that -native-compute no is needed seems unexpected: IIUC, the default -native-compiler ondemand means that no native code should be compiled, so where’s the extra time going?

8

It is expected that compiling Coq with flambda will be slower, you should measure Coq’s performance for user devs.

I don’t understand what you mean about -native-compute. With flambda and without flambda, you should use the default unless you are using < 4.07 then you need to workaround an OCaml bug.

9

That’s what we’re doing. Notice coq+flambda.org · GitHub talks about stdpp compile time. And that’s also what I measured; I’ve edited opam packages for that (tho I missed that early on).