Performance experiments

Gaëtan Gilbert edited this page Nov 7, 2018 · 4 revisions

This page is more for failed experiments, as successful ones can get merged (but feel free to add them here too ^^).

Skipping conversion of parameters of constructors and of the domain of lambdas (failed)

When converting fun x : A => e and fun x : A' => e' if I know they have the same type forall x : A, B I know that A == A' (Pi-injectivity).

Analogously when converting constructors we can skip parameters without breaking soundness.

The experiment fails because the kernel converts application arguments right to left, so if we have P : forall T, T -> ... and convert P (forall A0, ...) (fun x : A0' => ...) and P (forall A1, ...) (fun x : A1' => ...) we look at the lambdas before testing A0 == A1 (which by typing would imply A0' == A1'). This means skipping the lambda annotations skips a chance at early failure. Of course the same is true of skipping constructor parameters. Here's a partial bench: https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/391/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-mathcomp-field │  205.60  461.51  -55.45 % │  568829876254 1281746757731  -55.62 % │   819365613062 2059996916568 -60.22 % │  745460  814356 -8.46 % │   0   0  +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-real_closed │  117.40  172.82  -32.07 % │  324619461164  478365156189  -32.14 % │   436543675931  699685289928 -37.61 % │  811412  844848 -3.96 % │   0   0  +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│     coq-mathcomp-algebra │  157.57  185.61  -15.11 % │  435515533971  512539927127  -15.03 % │   559400684428  690239426679 -18.96 % │  643312  652328 -1.38 % │   0   0  +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-character │  255.34  275.70   -7.38 % │  707539906521  764571391145   -7.46 % │   986603630955 1085745868624  -9.13 % │ 1099132 1127652 -2.53 % │   0   5 -100.00 % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│    coq-mathcomp-fingroup │   60.84   64.40   -5.53 % │  167026713738  177626419100   -5.97 % │   218191435415  236222596014  -7.63 % │  588172  593152 -0.84 % │   0   0  +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│              coq-bignums │   79.67   80.06   -0.49 % │  219377009283  220962251825   -0.72 % │   283573204732  286100393647  -0.88 % │  529324  527276 +0.39 % │   0   0  +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-ssreflect │   44.67   44.67   +0.00 % │  121988881003  122288140972   -0.24 % │   141851033114  142842125752  -0.69 % │  536056  537640 -0.29 % │   0   0  +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│      coq-formal-topology │   37.55   37.42   +0.35 % │  100801859530  100686387892   +0.11 % │   125318244163  125809356994  -0.39 % │  483236  483448 -0.04 % │   0   0  +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│    coq-mathcomp-solvable │  230.96  201.62  +14.55 % │  639721848901  558026456354  +14.64 % │   889219447748  767706053248 +15.83 % │  840240  841228 -0.12 % │   0   0  +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-odd_order │ 2878.81 1427.47 +101.67 % │ 8004985597716 3963150813359 +101.99 % │ 12823742839111 6663549213977 +92.45 % │ 1406176 1391924 +1.02 % │   0   0  +nan % │
└──────────────────────────┴───────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴─────────────────┘

If we change the comparison order to left to right (as in #396) the above is alleviated but other places slow down to death: https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/393/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-mathcomp-field │  231.34  460.46 -49.76 % │  640657643986 1278240468084 -49.88 % │  938840609184 2059983208186 -54.42 % │  749856  814472 -7.93 % │   0   0  +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-real_closed │  128.33  172.62 -25.66 % │  354519892910  477561398004 -25.76 % │  485813524117  699666070629 -30.56 % │  820416  844836 -2.89 % │   0   0  +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│     coq-mathcomp-algebra │  165.87  184.82 -10.25 % │  457805151555  511415943712 -10.48 % │  596950648013  690197168687 -13.51 % │  647160  652284 -0.79 % │   0   0  +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│    coq-mathcomp-fingroup │   60.34   64.52  -6.48 % │  165936604399  177375464335  -6.45 % │  217866367230  236360925820  -7.82 % │  586992  593140 -1.04 % │   0   0  +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-ssreflect │   44.44   45.01  -1.27 % │  121629722412  122142651036  -0.42 % │  141930184433  142889177229  -0.67 % │  538080  537696 +0.07 % │   0   0  +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│              coq-bignums │   79.58   80.22  -0.80 % │  219446666227  220754218164  -0.59 % │  283500824146  286198520125  -0.94 % │  525864  527396 -0.29 % │   0   0  +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-odd_order │ 1491.34 1426.42  +4.55 % │ 4143753719381 3962374851065  +4.58 % │ 6959165055834 6663513117214  +4.44 % │ 1366556 1389552 -1.65 % │   0   0  +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│    coq-mathcomp-solvable │  211.22  201.86  +4.64 % │  584641881650  557846578469  +4.80 % │  822480782071  767855064436  +7.11 % │  878612  866188 +1.43 % │   0   0  +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-character │  293.63  275.63  +6.53 % │  814656149843  764490284216  +6.56 % │ 1167220824117 1085807185628  +7.50 % │ 1121104 1127156 -0.54 % │   0   0  +nan % │
└──────────────────────────┴──────────────────────────┴──────────────────────────────────────┴──────────────────────────────────────┴─────────────────────────┴─────────────────┘

after those developments formal topology didn't finish in ~8h (then I killed it). CI results for #396 at the time insinuate this may be in the corn dependency.

See https://github.com/SkySkimmer/coq/commit/1575ec75346a00955fd2f3f95179e958bbdc8b77 for implementation issues related to badly behaving callers.

Delay Universe Substitution in CClosure

See https://github.com/coq/coq/pull/8747.

┌──────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬──────────────────────────┬──────────────────────┐
│                          │      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-hott │  332.92  341.64 -2.55 % │   923345431138   946156146841 -2.41 % │  1406642863391  1440100985649 -2.32 % │  643632  666792  -3.47 % │  430    0     +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│                coq-sf-lf │   44.21   44.42 -0.47 % │   121743835280   122546861357 -0.66 % │   199315596414   199501609977 -0.09 % │  423608  422796  +0.19 % │  128    0     +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│                coq-flocq │  590.32  592.00 -0.28 % │  1640292423178  1647156759308 -0.42 % │  2411354196739  2405224361056 +0.25 % │ 1764632 1766556  -0.11 % │  606  867   -30.10 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│      coq-formal-topology │   58.08   58.24 -0.27 % │   158304951558   158865962983 -0.35 % │   239184450169   239985754037 -0.33 % │  477836  477416  +0.09 % │    0    0     +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│   coq-mathcomp-odd-order │ 1417.46 1420.48 -0.21 % │  3948768967038  3956033844700 -0.18 % │  6699320818703  6658637427858 +0.61 % │ 1350972 1359328  -0.61 % │  261   49  +432.65 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│             coq-compcert │  889.88  891.51 -0.18 % │  2467456059069  2470265840463 -0.11 % │  3578096037308  3561391545432 +0.47 % │ 1343276 1349328  -0.45 % │  617  339   +82.01 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│         coq-math-classes │  249.50  249.83 -0.13 % │   687224056760   688445471139 -0.18 % │   900867275902   899805525097 +0.12 % │  523152  522136  +0.19 % │   84   81    +3.70 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│         coq-fiat-parsers │  719.68  719.13 +0.08 % │  1998538693108  1996036522423 +0.13 % │  3080457738017  3054736560975 +0.84 % │ 2880308 2898680  -0.63 % │  590  761   -22.47 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│               coq-sf-plf │   74.76   74.68 +0.11 % │   206677543407   206541556383 +0.07 % │   301500338389   300926704664 +0.19 % │  521084  518568  +0.49 % │   15    0     +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│               coq-sf-vfa │   47.64   47.56 +0.17 % │   130990748145   131378232688 -0.29 % │   209993439783   209968706004 +0.01 % │  542076  533452  +1.62 % │   28    5  +460.00 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│            coq-fiat-core │  135.46  135.22 +0.18 % │   376724696562   377146921844 -0.11 % │   504668380099   504069509866 +0.12 % │  499292  497676  +0.32 % │  613  188  +226.06 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│   coq-mathcomp-ssreflect │   65.66   65.54 +0.18 % │   180023791228   180139505878 -0.06 % │   257095867228   256804442513 +0.11 % │  532368  532128  +0.05 % │   26  257   -89.88 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│          coq-fiat-crypto │ 6397.87 6379.31 +0.29 % │ 17792985556962 17744074236815 +0.28 % │ 29252536240733 29120658840711 +0.45 % │ 2723356 2450576 +11.13 % │ 1735 1347   +28.80 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│                coq-color │  740.67  738.32 +0.32 % │  2053660253546  2044831815430 +0.43 % │  2478563555420  2468606887351 +0.40 % │ 1371488 1375072  -0.26 % │   39  113   -65.49 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│    coq-mathcomp-fingroup │   85.43   85.12 +0.36 % │   236125046171   235251178827 +0.37 % │   350268845326   348848446344 +0.41 % │  594012  586388  +1.30 % │    4   48   -91.67 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│           coq-coquelicot │  104.28  103.85 +0.41 % │   287965548005   287163328551 +0.28 % │   388520908545   387043551167 +0.38 % │  725296  712312  +1.82 % │  282   13 +2069.23 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│                 coq-corn │ 1552.32 1545.75 +0.43 % │  4309382166395  4292619603160 +0.39 % │  6377647772888  6347727518034 +0.47 % │  926048  818152 +13.19 % │   45   60   -25.00 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│               coq-geocoq │ 2850.83 2838.13 +0.45 % │  7925675384464  7888923000596 +0.47 % │ 12703682815750 12579309110573 +0.99 % │ 1287824 1287704  +0.01 % │  606  190  +218.95 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│              coq-bignums │   99.47   98.88 +0.60 % │   274747249868   273697891152 +0.38 % │   394665541113   393829024474 +0.21 % │  536180  539500  -0.62 % │  175   43  +306.98 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│          coq-lambda-rust │ 2343.50 2329.46 +0.60 % │  6526599399602  6488604622730 +0.59 % │  9033098570801  8964156114014 +0.77 % │ 1544608 1450244  +6.51 % │  141   15  +840.00 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│   coq-mathcomp-character │  296.24  294.30 +0.66 % │   823620010282   817415400929 +0.76 % │  1197870057955  1191274757722 +0.55 % │ 1059976 1117428  -5.14 % │   45  302   -85.10 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│    coq-mathcomp-solvable │  222.11  220.18 +0.88 % │   617364103658   611819400697 +0.91 % │   882438288585   875349132855 +0.81 % │  807792  855168  -5.54 % │    2    1  +100.00 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│                  coq-vst │ 1728.61 1712.80 +0.92 % │  4806190843916  4762314463771 +0.92 % │  6562293639934  6513293300621 +0.75 % │ 2447808 2225288 +10.00 % │ 1166  868   +34.33 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│              coq-unimath │ 1343.67 1331.10 +0.94 % │  3731593916573  3693996753506 +1.02 % │  6317397679880  6240478754512 +1.23 % │ 1133008  971376 +16.64 % │  356   19 +1773.68 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│     coq-mathcomp-algebra │  208.10  205.23 +1.40 % │   577371493468   569418457780 +1.40 % │   810525479858   799120309546 +1.43 % │  648824  640676  +1.27 % │  293   14 +1992.86 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-mathcomp-real-closed │  190.92  188.10 +1.50 % │   531068217299   523597662881 +1.43 % │   804622480648   790375813147 +1.80 % │  853992  830204  +2.87 % │    1    1    +0.00 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│       coq-mathcomp-field │  475.01  467.97 +1.50 % │  1321459762740  1301256230599 +1.55 % │  2164466154596  2127074570257 +1.76 % │  805852  802264  +0.45 % │    2   19   -89.47 % │
└──────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┴──────────────────────┘
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.