Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Avoid roundtrip [fconstr] -> [constr] -> [fconstr] in the kernel #16497

Closed
wants to merge 6 commits into from
Closed

Avoid roundtrip [fconstr] -> [constr] -> [fconstr] in the kernel #16497

wants to merge 6 commits into from

Conversation

gmalecha
Copy link
Contributor

This is based on the discussion here: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/reduction.20in.20the.20kernel

It should be completely backwards compatible. I would like to get a benchmark run to determine if there is any impact. The code is a hackish right now (and contains some extra comments) just to test the potential performance difference, I will clean up before merge if we determine if it is useful.

  • Added / updated test-suite.

@gmalecha gmalecha requested a review from a team as a code owner September 15, 2022 15:36
@gmalecha gmalecha marked this pull request as draft September 15, 2022 15:37
@SkySkimmer
Copy link
Contributor

@coqbot bench

ppedrot
ppedrot reviewed Sep 15, 2022
View reviewed changes
kernel/reduction.ml Outdated Show resolved Hide resolved
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Sep 15, 2022

🏁 Bench results:

┌──────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬──────────────────────────┬─────────────────┐
│                              │      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-coqutil │   35.09    35.74  -1.82 │   157301202950    159798260137  -1.56 │   231443253068    231456985925  -0.01 │  601112   601048    0.01 │   1    1   0.00 │
│                   coq-stdlib │  419.59   425.75  -1.45 │  1776603387233   1795826619316  -1.07 │  1540100640584   1538716192811   0.09 │  696620   705184   -1.21 │   0    0    nan │
│                coq-fiat-core │   56.55    57.26  -1.24 │   240274479167    244165813768  -1.59 │   353437135889    353373276920   0.02 │  485824   485912   -0.02 │   2    0    nan │
│        coq-engine-bench-lite │  158.70   160.21  -0.94 │   676174091077    684394176003  -1.20 │  1288852488895   1291707047634  -0.22 │  982284   984848   -0.26 │   0    0    nan │
│         coq-metacoq-template │  131.41   132.45  -0.79 │   584253344004    589349853465  -0.86 │   968780090955    968669136019   0.01 │ 1283752  1287528   -0.29 │   0    0    nan │
│  coq-rewriter-perf-SuperFast │  755.42   759.95  -0.60 │  3378342758169   3405228522028  -0.79 │  5931704766819   5929386970036   0.04 │ 1243728  1243528    0.02 │ 160   89  79.78 │
│                  coq-bignums │   28.49    28.65  -0.56 │   128222207947    129261868621  -0.80 │   184876648562    184332528627   0.30 │  477676   475800    0.39 │   0    0    nan │
│                    coq-color │  225.48   226.47  -0.44 │  1008452035448   1014470293349  -0.59 │  1480968885672   1478402545015   0.17 │ 1184604  1184548    0.00 │   1    1   0.00 │
│   coq-performance-tests-lite │  772.49   775.82  -0.43 │  3449122270378   3465480783364  -0.47 │  6241977412131   6241832875823   0.00 │ 2434456  2430744    0.15 │ 481  332  44.88 │
│            coq-metacoq-pcuic │  572.43   574.83  -0.42 │  2582248337515   2592195340462  -0.38 │  3851073605861   3848889096724   0.06 │ 1954724  1955064   -0.02 │   0    0    nan │
│          coq-metacoq-erasure │  183.25   183.88  -0.34 │   822039020695    825616122743  -0.43 │  1337346025718   1336483526487   0.06 │ 1545344  1540876    0.29 │   0    0    nan │
│                 coq-coqprime │   43.95    44.05  -0.23 │   196239074188    197377889842  -0.58 │   303011317733    302066866543   0.31 │  765272   766888   -0.21 │   0    0    nan │
│                 coq-compcert │  294.81   295.15  -0.12 │  1324308225827   1323540045365   0.06 │  2047094098132   2046884955628   0.01 │ 1126528  1127700   -0.10 │  57    0    nan │
│                    coq-verdi │   47.61    47.60   0.02 │   214519086942    214327988042   0.09 │   330733131905    329266430017   0.45 │  790512   789264    0.16 │  30   16  87.50 │
│                   coq-flocq3 │   75.88    75.81   0.09 │   343001847870    342551566280   0.13 │   466659395785    464917063633   0.37 │ 1013452  1011960    0.15 │ 246    0    nan │
│                     coq-core │  112.14   111.85   0.26 │   464873367107    464643564410   0.05 │   485191150102    485483717960  -0.06 │  287556   286500    0.37 │   0    0    nan │
│ coq-fiat-crypto-with-bedrock │ 5732.47  5716.90   0.27 │ 25832687966249  25780209297810   0.20 │ 47355815658743  46986730506299   0.79 │ 3795168  3764756    0.81 │  86   87  -1.15 │
│                 coq-rewriter │  330.14   328.84   0.40 │  1494256871839   1488937634992   0.36 │  2517716680393   2510924095936   0.27 │ 1003068  1003352   -0.03 │   0    0    nan │
│                 coq-bedrock2 │  397.70   396.00   0.43 │  1783943849117   1772488355584   0.65 │  3462978214285   3448487712441   0.42 │ 1910068  1910112   -0.00 │  28    0    nan │
│      coq-metacoq-safechecker │  214.69   211.55   1.48 │   972197628026    957595837883   1.52 │  1448886486235   1447162008686   0.12 │ 1429136  1416036    0.93 │   0    0    nan │
│          coq-category-theory │  816.67   762.40   7.12 │  3702996847697   3463305262443   6.92 │  6440894947076   5986715545470   7.59 │ 1865304   924948  101.67 │ 188  167  12.57 │
└──────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┴─────────────────┘
🐢 Top 25 slow downs 
┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                   TOP 25 SLOW DOWNS                                                                   │
│                                                                                                                                                       │
│   OLD       NEW      DIFF      %DIFF     Ln                      FILE                                                                                 │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  32.3670   64.4950  32.1280     99.26%  1332  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html        │
│   0.1840   27.2180  27.0340  14692.39%    79  coq-category-theory/Theory/Coq/Applicative/Proofs.v.html                                                │
│   0.9570    4.8200   3.8630    403.66%   110  coq-category-theory/Construction/Comma/Adjunction.v.html                                                │
│   0.9500    4.8080   3.8580    406.11%   125  coq-category-theory/Construction/Comma/Adjunction.v.html                                                │
│ 132.5140  133.8280   1.3140      0.99%   706  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                             │
│  91.0750   92.2730   1.1980      1.32%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│   0.2760    1.2440   0.9680    350.72%   252  coq-category-theory/Functor/Structure/Monoidal/Compose.v.html                                           │
│   0.3360    1.2870   0.9510    283.04%    71  coq-category-theory/Structure/Monoidal/Product.v.html                                                   │
│   0.5030    1.4330   0.9300    184.89%   188  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/FancyMontgomeryReduction.v.html                    │
│  24.2930   25.2050   0.9120      3.75%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                                   │
│  52.5110   53.3710   0.8600      1.64%    50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│   0.1960    1.0430   0.8470    432.14%    89  coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Uppercase.v.html                            │
│   1.7390    2.5690   0.8300     47.73%  1087  coq-category-theory/Functor/Construction/Product/Monoidal.v.html                                        │
│  41.1250   41.9320   0.8070      1.96%   235  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                              │
│   1.2820    2.0800   0.7980     62.25%    33  coq-category-theory/Construction/Product/Comma.v.html                                                   │
│  10.0990   10.8120   0.7130      7.06%    53  coq-category-theory/Construction/Comma/Natural/Transformation.v.html                                    │
│   1.7560    2.4230   0.6670     37.98%    68  coq-category-theory/Instance/Cones/Comma.v.html                                                         │
│   3.8030    4.4550   0.6520     17.14%   775  coq-category-theory/Construction/Comma/Adjunction.v.html                                                │
│   4.1180    4.7670   0.6490     15.76%   129  coq-category-theory/Functor/Strong/Product.v.html                                                       │
│ 165.8020  166.3860   0.5840      0.35%   232  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  17.9810   18.5330   0.5520      3.07%  2032  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html        │
│  53.3540   53.8980   0.5440      1.02%    50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│   1.7120    2.2430   0.5310     31.02%   859  coq-category-theory/Functor/Construction/Product/Monoidal.v.html                                        │
│   9.7970   10.3160   0.5190      5.30%  1063  coq-metacoq-safechecker/safechecker/theories/PCUICSafeReduce.v.html                                     │
│  10.2850   10.7970   0.5120      4.98%   316  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                                │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SPEED UPS                                                               │
│                                                                                                                                              │
│   OLD       NEW      DIFF     %DIFF    Ln                     FILE                                                                           │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 132.2020  131.0670  -1.1350   -0.86%   992  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│ 132.0080  130.8890  -1.1190   -0.85%   962  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│  29.7170   29.0170  -0.7000   -2.36%   218  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html                                 │
│  25.1520   24.4790  -0.6730   -2.68%    19  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                         │
│   4.6300    3.9600  -0.6700  -14.47%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                           │
│  25.0850   24.4500  -0.6350   -2.53%    24  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                         │
│   3.8960    3.3530  -0.5430  -13.94%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                         │
│  29.1130   28.6420  -0.4710   -1.62%   352  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                               │
│  38.1350   37.6640  -0.4710   -1.24%   833  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                           │
│  61.2350   60.7870  -0.4480   -0.73%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                         │
│  14.8520   14.4440  -0.4080   -2.75%  2859  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                              │
│  48.8400   48.4390  -0.4010   -0.82%    66  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadder.v.html                  │
│  21.8590   21.4690  -0.3900   -1.78%   208  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                             │
│  15.9690   15.5790  -0.3900   -2.44%  3080  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                              │
│  16.1910   15.8200  -0.3710   -2.29%   258  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                               │
│   8.5910    8.2290  -0.3620   -4.21%  3151  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                              │
│  13.9210   13.5800  -0.3410   -2.45%   159  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                               │
│  52.8790   52.5420  -0.3370   -0.64%    84  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html                           │
│  13.0510   12.7150  -0.3360   -2.57%    14  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                         │
│  18.3450   18.0260  -0.3190   -1.74%   236  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v.html │
│ 138.3340  138.0170  -0.3170   -0.23%    47  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                          │
│  15.8950   15.6050  -0.2900   -1.82%  3148  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                              │
│  18.5960   18.3060  -0.2900   -1.56%   284  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v.html │
│   0.2880    0.0130  -0.2750  -95.49%   221  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/Cmd.v.html                     │
│  15.0780   14.8050  -0.2730   -1.81%   194  coq-fiat-crypto-with-bedrock/src/Demo.v.html                                                     │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@SkySkimmer
Copy link
Contributor

@coqbot bench

@SkySkimmer
Copy link
Contributor

Not sure how useful it wil be with this many failures

@gmalecha
Copy link
Contributor Author

Thanks. I'm going to try to look into the failures, they are all quite mysterious to me.

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Sep 16, 2022

🏁 Bench results:

┌────────────────────────────┬───────────────────────┬─────────────────────────────────────┬─────────────────────────────────────┬─────────────────────────┬─────────────────┐
│                            │     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-engine-bench-lite │ 159.01  160.19  -0.74 │  684378675122   690051829428  -0.82 │ 1303708878948  1297698650035   0.46 │  985788   980912   0.50 │   0    0    nan │
│              coq-fiat-core │  55.55   55.96  -0.73 │  241122195620   243399279698  -0.94 │  354197676835   350839166664   0.96 │  486796   484768   0.42 │   2    0    nan │
│                coq-coqutil │  35.15   35.40  -0.71 │  158730516140   160083652708  -0.85 │  232793603504   230648073143   0.93 │  602924   601028   0.32 │   1    1   0.00 │
│ coq-performance-tests-lite │ 764.21  768.79  -0.60 │ 3467557883277  3486444713106  -0.54 │ 6261871018765  6244844409793   0.27 │ 2431064  2434532  -0.14 │ 484  332  45.78 │
│                   coq-core │ 111.10  111.36  -0.23 │  467219343334   465427985223   0.38 │  485253720940   485101416942   0.03 │  287308   287504  -0.07 │   0    0    nan │
│                coq-bignums │  28.43   28.42   0.04 │  129394947072   129344839114   0.04 │  186427800600   184338924024   1.13 │  476276   475884   0.08 │   0    0    nan │
│                  coq-color │ 226.25  225.31   0.42 │ 1024603187595  1022036374113   0.25 │ 1498764230115  1474555061893   1.64 │ 1071020  1184608  -9.59 │   1    1   0.00 │
│               coq-coqprime │  43.99   43.80   0.43 │  199396065668   198611213224   0.40 │  307388141447   301928958337   1.81 │  767148   768412  -0.16 │   0    0    nan │
│                 coq-stdlib │ 423.90  420.72   0.76 │ 1815149461658  1791978494941   1.29 │ 1560125530820  1539620809880   1.33 │  687244   704628  -2.47 │   0    0    nan │
│               coq-bedrock2 │ 396.46  391.36   1.30 │ 1811910068476  1789092349370   1.28 │ 3509727261245  3447994251811   1.79 │ 1910092  1909964   0.01 │  28    0    nan │
│                 coq-flocq3 │  76.34   75.29   1.39 │  345943112268   341836954291   1.20 │  473228948408   464887090245   1.79 │ 1010320  1014984  -0.46 │ 246    0    nan │
│               coq-compcert │ 297.25  293.02   1.44 │ 1348250702673  1329886186248   1.38 │ 2080809542874  2047027416559   1.65 │ 1126960  1127572  -0.05 │  57    0    nan │
│                  coq-verdi │  48.62   47.17   3.07 │  221004247235   214936836415   2.82 │  340339726685   327317974881   3.98 │  789688   790148  -0.06 │  30   16  87.50 │
└────────────────────────────┴───────────────────────┴─────────────────────────────────────┴─────────────────────────────────────┴─────────────────────────┴─────────────────┘
🐢 Top 25 slow downs 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                    TOP 25 SLOW DOWNS                                                     │
│                                                                                                                          │
│   OLD      NEW     DIFF    %DIFF     Ln                 FILE                                                             │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  3.0300   3.9320  0.9020    29.77%  1891  coq-bedrock2/bedrock2/src/bedrock2Examples/LiveVerif/swap.v.html               │
│  1.7160   2.3880  0.6720    39.16%   843  coq-bedrock2/bedrock2/src/bedrock2Examples/LAN9250.v.html                      │
│  0.9530   1.5650  0.6120    64.22%   112  coq-bedrock2/bedrock2/src/bedrock2Examples/uint128_32.v.html                   │
│  1.3360   1.8190  0.4830    36.15%   563  coq-bedrock2/bedrock2/src/bedrock2Examples/LAN9250.v.html                      │
│ 40.2710  40.7090  0.4380     1.09%   222  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html │
│  1.9500   2.3550  0.4050    20.77%   706  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                │
│  1.8550   2.1480  0.2930    15.80%   512  coq-color/Term/Lambda/LCompClos.v.html                                         │
│  1.6430   1.9240  0.2810    17.10%   373  coq-bedrock2/bedrock2/src/bedrock2Examples/memmove.v.html                      │
│ 14.9370  15.2010  0.2640     1.77%    29  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                      │
│  3.2300   3.4920  0.2620     8.11%  1945  coq-bedrock2/bedrock2/src/bedrock2Examples/LiveVerif/swap.v.html               │
│  0.8970   1.1040  0.2070    23.08%   166  coq-bedrock2/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v.html            │
│  0.3980   0.5730  0.1750    43.97%   638  coq-bedrock2/bedrock2/src/bedrock2Examples/SPI_live.v.html                     │
│  0.3780   0.5370  0.1590    42.06%   371  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                    │
│  0.5910   0.7410  0.1500    25.38%   251  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                    │
│  1.0830   1.2220  0.1390    12.83%   119  coq-bedrock2/bedrock2/src/bedrock2Examples/bsearch.v.html                      │
│  0.0290   0.1660  0.1370   472.41%   357  coq-color/Term/Lambda/LCompClos.v.html                                         │
│  0.4400   0.5580  0.1180    26.82%   220  coq-bedrock2/bedrock2/src/bedrock2Examples/SPI.v.html                          │
│  0.3560   0.4700  0.1140    32.02%   376  coq-bedrock2/bedrock2/src/bedrock2Examples/SPI.v.html                          │
│  0.0420   0.1500  0.1080   257.14%  1902  coq-bedrock2/bedrock2/src/bedrock2Examples/LiveVerif/swap.v.html               │
│  0.0920   0.1900  0.0980   106.52%   495  coq-fiat-core/src/Common/Wf2.v.html                                            │
│  0.0050   0.1030  0.0980  1960.00%   438  coq-color/Term/WithArity/AMatching.v.html                                      │
│  0.2800   0.3730  0.0930    33.21%   304  coq-bedrock2/bedrock2/src/bedrock2Examples/LAN9250.v.html                      │
│  0.0000   0.0920  0.0920      inf%  9704  coq-coqprime/src/Coqprime/examples/BasePrimes.v.html                           │
│  0.0000   0.0900  0.0900      inf%   414  coq-color/DP/ASCCUnion.v.html                                                  │
│  0.1580   0.2470  0.0890    56.33%   249  coq-color/DP/ASCCUnion.v.html                                                  │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                       TOP 25 SPEED UPS                                                       │
│                                                                                                                              │
│   OLD       NEW      DIFF     %DIFF     Ln                  FILE                                                             │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 129.9280  128.8840  -1.0440    -0.80%   992  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│ 129.7070  128.7370  -0.9700    -0.75%   962  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│   3.8220    3.5030  -0.3190    -8.35%     5  coq-engine-bench-lite/coq/PerformanceDemos/repeated_conj.v.html                 │
│   8.6060    8.4120  -0.1940    -2.25%    84  coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html           │
│  14.5200   14.3290  -0.1910    -1.32%    30  coq-performance-tests-lite/src/pattern.v.html                                   │
│   5.4290    5.2520  -0.1770    -3.26%   619  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│   2.9210    2.7580  -0.1630    -5.58%   994  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│   1.0990    0.9370  -0.1620   -14.74%   514  coq-color/Term/Lambda/LCompClos.v.html                                          │
│   0.3390    0.1790  -0.1600   -47.20%   167  coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html           │
│  21.7010   21.5690  -0.1320    -0.61%   318  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html            │
│   0.4710    0.3490  -0.1220   -25.90%   251  coq-color/Term/Lambda/LSystemT.v.html                                           │
│  21.7870   21.6690  -0.1180    -0.54%   208  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html            │
│  44.5550   44.4410  -0.1140    -0.26%   578  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                 │
│   6.7450    6.6350  -0.1100    -1.63%    29  coq-performance-tests-lite/src/pattern.v.html                                   │
│   3.2480    3.1390  -0.1090    -3.36%    33  coq-engine-bench-lite/coq/PerformanceDemos/rewrite_strat_repeated_app.v.html    │
│   6.5160    6.4070  -0.1090    -1.67%   702  coq-bedrock2/bedrock2/src/bedrock2Examples/LAN9250.v.html                       │
│   0.2430    0.1400  -0.1030   -42.39%   371  coq-color/Term/Lambda/LCompClos.v.html                                          │
│   0.0990    0.0000  -0.0990  -100.00%   469  coq-color/Term/WithArity/AMatching.v.html                                       │
│   9.5460    9.4500  -0.0960    -1.01%    47  coq-bedrock2/bedrock2/src/bedrock2/WeakestPreconditionProperties.v.html         │
│   2.5620    2.4700  -0.0920    -3.59%     5  coq-engine-bench-lite/coq/PerformanceDemos/repeated_conj.v.html                 │
│   0.1380    0.0470  -0.0910   -65.94%   192  coq-color/DP/ASCCUnion.v.html                                                   │
│   0.0890    0.0010  -0.0880   -98.88%   739  coq-color/Term/Lambda/LTerm.v.html                                              │
│   0.0990    0.0120  -0.0870   -87.88%   497  coq-color/Term/Lambda/LCall.v.html                                              │
│   0.0870    0.0000  -0.0870  -100.00%  8311  coq-coqprime/src/Coqprime/examples/BasePrimes.v.html                            │
│   0.0870    0.0000  -0.0870  -100.00%   456  coq-color/Term/Lambda/LSimple.v.html                                            │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@gmalecha
Copy link
Contributor Author

The latest change fixed most of the issues. I'm not sure about fiat-crypto, but unimath is a timeout. This seems to suggest that the cost of maintaining sharing is too high compared to the (hypothetical) benefit. It might be possible to regain some efficiency with a lazy copy.

@SkySkimmer
Copy link
Contributor

@coqbot bench

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Sep 19, 2022

🏁 Bench results:

┌────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬──────────────────────────┬───────────────────┐
│                            │      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-core │  145.67   147.23  -1.06 │   457827200080    460159573714  -0.51 │   484903300052    485310353217  -0.08 │  286884   286232    0.23 │   1    0      nan │
│      coq-engine-bench-lite │  202.49   203.40  -0.45 │   845530820271    849495815938  -0.47 │  1305799755277   1303215297289   0.20 │  981404   981976   -0.06 │   0    0      nan │
│ coq-performance-tests-lite │  952.78   952.68   0.01 │  4016676886474   4004906308585   0.29 │  6305782635523   6256897797654   0.78 │ 2431036  2434684   -0.15 │   3    0      nan │
│              coq-fourcolor │ 1772.65  1769.09   0.20 │  7596603795168   7582182528386   0.19 │ 12316157838590  12222705472459   0.76 │  737208   738964   -0.24 │   0    0      nan │
│              coq-fiat-core │   69.13    68.52   0.89 │   278142786307    275934603534   0.80 │   371542511618    361627941614   2.74 │  485560   484692    0.18 │   2    4   -50.00 │
│                coq-coqutil │   43.98    43.45   1.22 │   183675126428    180802028863   1.59 │   244337526401    236650185339   3.25 │  600940   601068   -0.02 │   0    0      nan │
│               coq-compcert │  364.80   359.05   1.60 │  1531796546367   1505648740557   1.74 │  2177598542821   2056484841879   5.89 │ 1127976  1126564    0.13 │   0   50  -100.00 │
│                 coq-geocoq │  909.22   893.23   1.79 │  3813075411765   3751559746784   1.64 │  5481577932282   5315694430325   3.12 │ 1010924  1104792   -8.50 │   0    0      nan │
│                 coq-stdlib │  552.69   542.94   1.80 │  1770244289834   1735077143150   2.03 │  1614324605177   1539942306727   4.83 │  720408   708500    1.68 │   0    0      nan │
│           coq-math-classes │  117.29   114.96   2.03 │   489592450239    480733928043   1.84 │   666742296951    643631438004   3.59 │  513292   513740   -0.09 │   0    0      nan │
│                coq-bignums │   34.36    33.66   2.08 │   144276797966    141353911268   2.07 │   190561039998    184309751629   3.39 │  476260   479272   -0.63 │   2    0      nan │
│               coq-bedrock2 │  526.01   512.92   2.55 │  2229031281080   2171629003385   2.64 │  3596540003666   3469603445906   3.66 │ 1910120  1910332   -0.01 │   7    0      nan │
│                  coq-color │  284.18   275.99   2.97 │  1185984086616   1150044961995   3.13 │  1592863766159   1495929380430   6.48 │ 1071164  1184516   -9.57 │   1    1     0.00 │
│               coq-coqprime │   54.98    53.20   3.35 │   230329675348    222484337468   3.53 │   320188390283    304598418901   5.12 │  765804   765732    0.01 │   0    0      nan │
│                   coq-corn │ 1003.10   965.37   3.91 │  4215475977348   4053814757798   3.99 │  6163756004699   5843187380046   5.49 │  928876   862660    7.68 │   0    0      nan │
│           coq-fiat-parsers │  437.19   420.08   4.07 │  1833641467175   1764728095065   3.91 │  2719345335451   2560267830881   6.21 │ 3163004  3539088  -10.63 │   0    0      nan │
│                 coq-flocq3 │   94.43    90.46   4.39 │   393414608683    377662183842   4.17 │   500724672254    469586360869   6.63 │ 1010056  1010124   -0.01 │   4    0      nan │
│             coq-verdi-raft │  744.70   704.78   5.66 │  3106400673420   2942361148276   5.58 │  4561175838014   4215023318410   8.21 │ 1227716  1232100   -0.36 │   0    0      nan │
│             coq-coquelicot │   45.75    43.15   6.03 │   190451093800    180220322209   5.68 │   243086654957    222661425025   9.17 │  749960   745992    0.53 │  84    0      nan │
│     coq-mathcomp-odd-order │  596.08   558.98   6.64 │  2495844162305   2336420799697   6.82 │  4041762706357   3745004727087   7.92 │  961448   961508   -0.01 │   0    0      nan │
│                   coq-hott │  204.50   191.40   6.84 │   853415307130    799721401179   6.71 │  1291184578372   1176078989172   9.79 │  574580   578972   -0.76 │   0    0      nan │
│     coq-mathcomp-ssreflect │   33.54    31.22   7.43 │   141078659861    131654964703   7.16 │   176175428822    157503627790  11.85 │  566804   564828    0.35 │   1    0      nan │
│          coq-iris-examples │  631.62   585.40   7.90 │  2648287354469   2454446328629   7.90 │  3735345829466   3371844923139  10.78 │ 1226708  1222168    0.37 │   0    0      nan │
│                  coq-verdi │   62.40    57.40   8.71 │   261401737794    240136124658   8.86 │   371819694296    331634726167  12.12 │  790544   791060   -0.07 │   0    0      nan │
│       coq-mathcomp-algebra │   80.12    73.30   9.30 │   337850517312    308554659864   9.49 │   452164065815    396465287189  14.05 │  573032   571536    0.26 │   0    0      nan │
│         coq-mathcomp-field │  125.63   114.31   9.90 │   526891686407    479970570709   9.78 │   805554841228    715472638468  12.59 │  651624   651544    0.01 │   0    0      nan │
│              coq-perennial │ 6547.54  5954.15   9.97 │ 27453685004254  24973865099085   9.93 │ 42431355252011  37522687414532  13.08 │ 2715376  2698848    0.61 │   0    1  -100.00 │
│     coq-mathcomp-character │   90.56    81.79  10.72 │   380746939398    342633645974  11.12 │   555582217193    478944568051  16.00 │  750156   750284   -0.02 │   0    0      nan │
│      coq-mathcomp-solvable │  108.90    98.28  10.81 │   457666238624    413002383373  10.81 │   668033819196    582127910445  14.76 │  667032   664168    0.43 │   0    0      nan │
│      coq-mathcomp-fingroup │   29.97    26.93  11.29 │   126120851010    113237434412  11.38 │   178980681921    152821690684  17.12 │  499952   495168    0.97 │   0    0      nan │
└────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┴───────────────────┘
🐢 Top 25 slow downs 
┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                   TOP 25 SLOW DOWNS                                                   │
│                                                                                                                       │
│   OLD      NEW     DIFF     %DIFF    Ln                 FILE                                                          │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 43.4810  67.2740  23.7930   54.72%   521  coq-perennial/src/program_proof/txn/twophase_refinement_proof.v.html        │
│  1.8600  16.4640  14.6040  785.16%   988  coq-perennial/src/program_proof/buf/buf_proof.v.html                        │
│ 28.0570  41.7860  13.7290   48.93%  2290  coq-perennial/src/goose_lang/logical_reln_fund.v.html                       │
│ 25.8210  39.4070  13.5860   52.62%   606  coq-perennial/src/program_proof/simplepb/pb_apply_proof.v.html              │
│ 28.1020  41.2940  13.1920   46.94%  1354  coq-perennial/src/program_proof/wal/installer_proof.v.html                  │
│ 27.1400  39.6400  12.5000   46.06%  1153  coq-perennial/src/program_proof/simplepb/admin_proof.v.html                 │
│ 25.8900  37.4150  11.5250   44.52%   267  coq-perennial/src/program_proof/memkv/memkv_coord_start_proof.v.html        │
│ 22.8310  33.2740  10.4430   45.74%   874  coq-perennial/src/program_proof/simple/setattr.v.html                       │
│ 25.1960  34.3700   9.1740   36.41%   812  coq-perennial/src/program_proof/wal/logger_proof.v.html                     │
│ 15.6860  23.8920   8.2060   52.31%  1381  coq-perennial/src/program_proof/txn/twophase_sub_logical_reln_defs.v.html   │
│ 14.5010  21.7910   7.2900   50.27%   414  coq-perennial/src/program_proof/simplepb/pb_becomeprimary_proof.v.html      │
│  0.8800   8.0350   7.1550  813.07%   932  coq-perennial/src/program_proof/buf/buf_proof.v.html                        │
│ 12.7260  19.6780   6.9520   54.63%   641  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html              │
│ 14.7220  21.1420   6.4200   43.61%   461  coq-perennial/src/program_proof/simple/write.v.html                         │
│ 10.8980  16.7210   5.8230   53.43%  1009  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html              │
│ 10.3530  15.7260   5.3730   51.90%  1469  coq-perennial/src/program_proof/obj/commit_proof.v.html                     │
│ 10.4670  15.1650   4.6980   44.88%  1504  coq-perennial/src/program_proof/wal/recovery_proof.v.html                   │
│ 10.0870  14.7220   4.6350   45.95%   579  coq-perennial/src/program_proof/simple/read.v.html                          │
│  7.7880  12.2670   4.4790   57.51%   882  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html              │
│  8.6400  13.0860   4.4460   51.46%   925  coq-perennial/src/program_proof/wal/write_proof.v.html                      │
│  9.5060  13.8050   4.2990   45.22%  1020  coq-perennial/src/program_proof/examples/async_mem_alloc_inode_proof.v.html │
│  9.2830  13.5770   4.2940   46.26%   281  coq-perennial/src/program_proof/memkv/memkv_shard_start_proof.v.html        │
│  7.9500  11.9910   4.0410   50.83%   575  coq-perennial/src/program_proof/simple/getattr.v.html                       │
│  8.0790  11.9280   3.8490   47.64%   419  coq-perennial/src/program_proof/crash_lockmap_proof.v.html                  │
│  7.5220  11.3560   3.8340   50.97%  1582  coq-perennial/src/program_proof/fencing/ctr_proof.v.html                    │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                      TOP 25 SPEED UPS                                                       │
│                                                                                                                             │
│   OLD       NEW      DIFF     %DIFF    Ln                  FILE                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 162.9590  161.1400  -1.8190   -1.12%   962  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│ 163.7440  162.0070  -1.7370   -1.06%   992  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│  82.4320   81.3810  -1.0510   -1.27%   137  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                    │
│  35.6310   34.9570  -0.6740   -1.89%  1375  coq-fourcolor/theories/cfmap.v.html                                             │
│  30.9640   30.3980  -0.5660   -1.83%    10  coq-fourcolor/theories/job495to498.v.html                                       │
│   0.5700    0.1330  -0.4370  -76.67%  1173  coq-perennial/src/program_proof/wal/recovery_proof.v.html                       │
│   0.4410    0.0280  -0.4130  -93.65%   557  coq-perennial/src/program_logic/staged_invariant_use_inuse2.v.html              │
│   1.2710    0.8750  -0.3960  -31.16%  1906  coq-perennial/src/program_proof/wal/recovery_proof.v.html                       │
│  19.2780   18.8890  -0.3890   -2.02%    30  coq-performance-tests-lite/src/pattern.v.html                                   │
│  29.0810   28.7090  -0.3720   -1.28%   318  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html            │
│  32.2530   31.8960  -0.3570   -1.11%    10  coq-fourcolor/theories/job319to322.v.html                                       │
│  19.2610   18.9090  -0.3520   -1.83%    29  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                       │
│  34.6510   34.3330  -0.3180   -0.92%    10  coq-fourcolor/theories/job531to534.v.html                                       │
│   6.2790    5.9690  -0.3100   -4.94%   555  coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/fundamental.v.html       │
│  21.3220   21.0270  -0.2950   -1.38%   185  coq-perennial/src/goose_lang/interpreter/disk_interpreter.v.html                │
│  30.9880   30.7010  -0.2870   -0.93%    10  coq-fourcolor/theories/job295to298.v.html                                       │
│  32.2500   31.9650  -0.2850   -0.88%    10  coq-fourcolor/theories/job503to506.v.html                                       │
│  33.1650   32.8800  -0.2850   -0.86%    10  coq-fourcolor/theories/job223to226.v.html                                       │
│  35.6060   35.3290  -0.2770   -0.78%    10  coq-fourcolor/theories/job287to290.v.html                                       │
│  29.0550   28.7870  -0.2680   -0.92%   208  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html            │
│  32.7640   32.5040  -0.2600   -0.79%    10  coq-fourcolor/theories/job227to230.v.html                                       │
│   6.3240    6.0750  -0.2490   -3.94%   649  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│  33.0000   32.7550  -0.2450   -0.74%    10  coq-fourcolor/theories/job279to282.v.html                                       │
│   0.3000    0.0720  -0.2280  -76.00%    91  coq-perennial/src/program_proof/simple/common.v.html                            │
│  11.9580   11.7430  -0.2150   -1.80%   194  coq-perennial/src/program_proof/simplepb/pb_applybackup_proof.v.html            │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@Alizter
Copy link
Contributor

Alizter commented Sep 19, 2022

Those slowdowns in prennial are looking pretty worrying. I wonder why they are happening.

│   OLD      NEW     DIFF     %DIFF    Ln                 FILE                                                          │
│ 43.4810  67.2740  23.7930   54.72%   521  coq-perennial/src/program_proof/txn/twophase_refinement_proof.v.html        │
│  1.8600  16.4640  14.6040  785.16%   988  coq-perennial/src/program_proof/buf/buf_proof.v.html                        │
│ 28.0570  41.7860  13.7290   48.93%  2290  coq-perennial/src/goose_lang/logical_reln_fund.v.html

@gmalecha
Copy link
Contributor Author

@Alizter the issue is that the copy of the fconstr is too expensive to be justified by the savings from sharing in most cases. I don't think this will get merged unless there is a way to speed that up a lot.

@ppedrot
Copy link
Member

ppedrot commented Sep 19, 2022

This is indeed starting to look like a failed experiment...

@gmalecha
Copy link
Contributor Author

@ppedrot I concur. My current take is that copy_fconstr is much more expensive than inject (to_constr ..). The later loses sharing, the former does not. Do you think there could be a way to speed up the copy operation either by making it lazier or by memoizing larger-grained pieces of the copy?

@gmalecha gmalecha mentioned this pull request Oct 1, 2022
Closed
2 tasks
@ppedrot
Copy link
Member

ppedrot commented Oct 14, 2022

Closing this, since this PR seems to fulfilled its goal.

@ppedrot ppedrot closed this Oct 14, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@gmalecha @SkySkimmer @Alizter @ppedrot