ppedrot
commented
2 weeks ago @coqbot bench
Closed ppedrot closed 2 weeks ago
ppedrot
commented
2 weeks ago @coqbot bench
SkySkimmer
commented
2 weeks ago We also introduce a cache internal to this function to only compute the expansion once.
Is this out of caution or was there a case where it noticeably helped?
ppedrot
commented
2 weeks ago It actually helped on the compcert example.
coqbot-app[bot]
commented
2 weeks ago :checkered_flag: Bench results:
┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│ │ user time [s] │ CPU cycles │ CPU instructions │ max resident mem [KB] │
│ │ │ │ │ │
│ package_name │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│ coq-mathcomp-fingroup │ 30.18 30.59 -1.34 │ 137035719931 139007191747 -1.42 │ 207755265572 207781430313 -0.01 │ 568976 568316 0.12 │
│ coq-stdlib │ 352.22 356.32 -1.15 │ 1477200167758 1485801166616 -0.58 │ 1258588799429 1258527421586 0.00 │ 715596 719976 -0.61 │
│ coq-metacoq-translations │ 16.95 17.14 -1.11 │ 75048207957 75478300416 -0.57 │ 125128126162 125091865139 0.03 │ 847148 846336 0.10 │
│ coq-bignums │ 29.51 29.79 -0.94 │ 133351919497 134247747752 -0.67 │ 192283642732 192278518602 0.00 │ 478244 480232 -0.41 │
│ coq-metacoq-safechecker │ 419.75 423.67 -0.93 │ 1913703764663 1932811066651 -0.99 │ 3184384814573 3184592713017 -0.01 │ 2076760 2075000 0.08 │
│ coq-performance-tests-lite │ 710.24 714.01 -0.53 │ 3177792644196 3194303356032 -0.52 │ 5684649573768 5684843371587 -0.00 │ 2276100 2276376 -0.01 │
│ coq-equations │ 7.65 7.69 -0.52 │ 31236693417 31204112003 0.10 │ 50910961508 50986969065 -0.15 │ 389712 388108 0.41 │
│ coq-math-classes │ 85.53 85.88 -0.41 │ 382990888448 384508579177 -0.39 │ 536943595394 536973069036 -0.01 │ 503524 504064 -0.11 │
│ coq-iris-examples │ 467.97 469.84 -0.40 │ 2117484941679 2125836818786 -0.39 │ 3275826295181 3276880810567 -0.03 │ 1119656 1114056 0.50 │
│ coq-vst │ 880.71 884.16 -0.39 │ 3982529961896 3996658281030 -0.35 │ 6740934469046 6744059408577 -0.05 │ 2164764 2166308 -0.07 │
│ coq-fiat-parsers │ 312.55 313.73 -0.38 │ 1384290332000 1389901871852 -0.40 │ 2471229003670 2471329704967 -0.00 │ 2408944 2407084 0.08 │
│ coq-metacoq-pcuic │ 987.49 991.14 -0.37 │ 4405485501724 4420222087721 -0.33 │ 6468607847354 6469937276154 -0.02 │ 2678168 2679616 -0.05 │
│ coq-coqprime │ 48.18 48.35 -0.35 │ 215365793815 216039798846 -0.31 │ 334435525664 334469727391 -0.01 │ 786500 785440 0.13 │
│ coq-test-suite │ 703.15 705.36 -0.31 │ 2989827258271 2994044840525 -0.14 │ 5370220601732 5374566974083 -0.08 │ 2469064 2695752 -8.41 │
│ coq-bedrock2 │ 363.33 364.39 -0.29 │ 1646126565306 1644390723592 0.11 │ 3110597766112 3110357424733 0.01 │ 858292 857924 0.04 │
│ coq-compcert │ 281.90 282.71 -0.29 │ 1267293324237 1269566926701 -0.18 │ 1945584641412 1945663371998 -0.00 │ 1124336 1123836 0.04 │
│ coq-metacoq-template │ 151.14 151.56 -0.28 │ 665156199206 667870027405 -0.41 │ 1046889415082 1046886319362 0.00 │ 1512680 1511800 0.06 │
│ coq-neural-net-interp-computed-lite │ 298.90 299.65 -0.25 │ 1363206144777 1366246755953 -0.22 │ 3617714590486 3617741653668 -0.00 │ 1114960 1114644 0.03 │
│ coq-metacoq-erasure │ 504.72 505.98 -0.25 │ 2284098598352 2292004670640 -0.34 │ 3581721548182 3581572815444 0.00 │ 2102116 2104288 -0.10 │
│ coq-rewriter-perf-SuperFast │ 796.51 797.82 -0.16 │ 3560093960954 3562925231367 -0.08 │ 6256333072490 6256524837982 -0.00 │ 1574496 1572008 0.16 │
│ coq-corn │ 717.12 717.95 -0.12 │ 3241508454596 3246801215655 -0.16 │ 5077842140099 5077860498013 -0.00 │ 755308 755196 0.01 │
│ coq-mathcomp-character │ 109.98 110.08 -0.09 │ 500007083623 500322869816 -0.06 │ 790438279101 790424171832 0.00 │ 1136024 1136356 -0.03 │
│ coq-verdi │ 49.29 49.33 -0.08 │ 220567479140 220960415891 -0.18 │ 340853552949 340860291290 -0.00 │ 531320 531296 0.00 │
│ coq-fiat-core │ 60.03 60.05 -0.03 │ 246865644979 247724149784 -0.35 │ 368675428688 368685138812 -0.00 │ 487196 482480 0.98 │
│ coq-verdi-raft │ 582.01 581.96 0.01 │ 2639198608670 2642930483468 -0.14 │ 4161481056857 4162636341324 -0.03 │ 848308 847804 0.06 │
│ coq-fourcolor │ 1369.71 1369.32 0.03 │ 6231985140666 6231244320557 0.01 │ 12909591024222 12909638500859 -0.00 │ 2137636 2137672 -0.00 │
│ coq-fiat-crypto-with-bedrock │ 6246.94 6243.39 0.06 │ 28309635783422 28286886542210 0.08 │ 51230106225076 51230539440561 -0.00 │ 3245844 3246092 -0.01 │
│ coq-color │ 252.09 251.90 0.08 │ 1125930539545 1124880837733 0.09 │ 1635991476524 1635897391327 0.01 │ 1175576 1178408 -0.24 │
│ coq-unimath │ 2467.00 2464.93 0.08 │ 11187255653341 11177143485611 0.09 │ 22209897548767 22210691259119 -0.00 │ 1254624 1254268 0.03 │
│ coq-core │ 130.20 130.07 0.10 │ 498935635394 500890277700 -0.39 │ 531991518532 531685390393 0.06 │ 458068 457808 0.06 │
│ coq-mathcomp-solvable │ 118.19 117.92 0.23 │ 537618064900 537338612266 0.05 │ 857112188662 857160851171 -0.01 │ 880000 877340 0.30 │
│ coq-rewriter │ 392.37 391.28 0.28 │ 1768283040970 1765528100185 0.16 │ 2990719325516 2990577267455 0.00 │ 1478004 1477272 0.05 │
│ coq-hott │ 161.56 160.95 0.38 │ 714578562906 713522504547 0.15 │ 1140274842989 1140279515244 -0.00 │ 477792 477884 -0.02 │
│ coq-category-theory │ 696.65 693.65 0.43 │ 3154784446499 3143870763807 0.35 │ 5260327245310 5260814305566 -0.01 │ 958004 955752 0.24 │
│ coq-mathcomp-field │ 144.17 143.39 0.54 │ 651074940651 646330445607 0.73 │ 1074425973242 1074371171524 0.01 │ 1483376 1483976 -0.04 │
│ coq-mathcomp-algebra │ 262.09 260.62 0.56 │ 1184281203310 1178461621513 0.49 │ 2000704456809 2000714593705 -0.00 │ 1332448 1331276 0.09 │
│ coq-coqutil │ 42.77 42.48 0.68 │ 186948525043 186926611274 0.01 │ 270864763122 270855795671 0.00 │ 561076 561368 -0.05 │
│ coq-coquelicot │ 39.93 39.55 0.96 │ 176598599640 176072213294 0.30 │ 248996589565 249016409476 -0.01 │ 852740 852240 0.06 │
│ coq-engine-bench-lite │ 158.29 156.73 1.00 │ 663272099169 656288950458 1.06 │ 1223980620598 1222518649770 0.12 │ 1324076 1321608 0.19 │
│ coq-mathcomp-odd-order │ 793.89 785.56 1.06 │ 3623724575472 3587220222056 1.02 │ 6078852539732 6078820385850 0.00 │ 1657116 1655200 0.12 │
│ coq-mathcomp-ssreflect │ 224.69 221.37 1.50 │ 1013248339782 998101199961 1.52 │ 1675944031191 1675942351090 0.00 │ 1720780 1718436 0.14 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 77.2960 82.7070 5.4110 7.00% 365 coq-mathcomp-odd-order/theories/PFsection4.v.html │ │ 64.2430 68.7550 4.5120 7.02% 368 coq-mathcomp-odd-order/theories/PFsection4.v.html │ │ 96.1370 97.1240 0.9870 1.03% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 46.6070 47.3610 0.7540 1.62% 926 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html │ │ 13.9810 14.7320 0.7510 5.37% 12 coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html │ │ 131.9630 132.6440 0.6810 0.52% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 45.9310 46.5770 0.6460 1.41% 110 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 11.3440 11.8930 0.5490 4.84% 2103 coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html │ │ 21.4480 21.9830 0.5350 2.49% 376 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.v.html │ │ 37.4030 37.9180 0.5150 1.38% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 27.5900 28.0440 0.4540 1.65% 1933 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v.html │ │ 38.4770 38.9020 0.4250 1.10% 338 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 33.4820 33.9050 0.4230 1.26% 1333 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 3.4350 3.8520 0.4170 12.14% 884 coq-mathcomp-odd-order/theories/BGsection16.v.html │ │ 23.8510 24.2660 0.4150 1.74% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 72.8270 73.2390 0.4120 0.57% 905 coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html │ │ 37.5330 37.9420 0.4090 1.09% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v.html │ │ 19.6870 20.0610 0.3740 1.90% 325 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 19.7900 20.1560 0.3660 1.85% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 7.0770 7.4110 0.3340 4.72% 2089 coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html │ │ 2.5250 2.8580 0.3330 13.19% 812 coq-mathcomp-odd-order/theories/BGsection16.v.html │ │ 22.0800 22.4020 0.3220 1.46% 2061 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 27.0970 27.3730 0.2760 1.02% 68 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │ │ 35.8990 36.1750 0.2760 0.77% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 24.6670 24.9370 0.2700 1.09% 375 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 219.8580 217.2770 -2.5810 -1.17% 103 coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html │ │ 64.7730 63.0590 -1.7140 -2.65% 609 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 243.2090 241.7010 -1.5080 -0.62% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 181.5120 180.3860 -1.1260 -0.62% 233 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │ │ 155.2790 154.1890 -1.0900 -0.70% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 64.5500 63.5850 -0.9650 -1.49% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 257.8520 257.0140 -0.8380 -0.32% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 138.9790 138.3210 -0.6580 -0.47% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 12.6570 11.9990 -0.6580 -5.20% 194 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 2.9910 2.3860 -0.6050 -20.23% 487 coq-stdlib/Numbers/HexadecimalFacts.v.html │ │ 256.2630 255.6610 -0.6020 -0.23% 1629 coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html │ │ 48.5150 47.9900 -0.5250 -1.08% 558 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 47.1890 46.7650 -0.4240 -0.90% 110 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 4.1600 3.8240 -0.3360 -8.08% 1444 coq-metacoq-erasure/erasure/theories/ErasureFunction.v.html │ │ 95.9550 95.6420 -0.3130 -0.33% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 18.6770 18.3800 -0.2970 -1.59% 12 coq-fourcolor/theories/job207to214.v.html │ │ 95.8880 95.6000 -0.2880 -0.30% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 102.2030 101.9150 -0.2880 -0.28% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 1.6770 1.3950 -0.2820 -16.82% 60 coq-vst/veric/tcb.v.html │ │ 0.6100 0.3280 -0.2820 -46.23% 868 coq-stdlib/MSets/MSetRBT.v.html │ │ 14.9490 14.6710 -0.2780 -1.86% 490 coq-unimath/UniMath/HomologicalAlgebra/KA.v.html │ │ 26.8970 26.6280 -0.2690 -1.00% 22 coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html │ │ 17.4550 17.1860 -0.2690 -1.54% 472 coq-metacoq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v.html │ │ 4.8480 4.5910 -0.2570 -5.30% 320 coq-metacoq-erasure/erasure/theories/ErasureProperties.v.html │ │ 0.9140 0.6650 -0.2490 -27.24% 813 coq-stdlib/MSets/MSetRBT.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
ppedrot
commented
2 weeks ago I think that the bench basically doesn't measure anything coqchk-related. The current run is just noise. But on the one-liner from compcert this PR reduces the coqchk invocation from ~87s to ~78s, and the perf profile shows that it removes the dominating trace of module substitution.
SkySkimmer
commented
2 weeks ago @coqbot merge now
Rather than folding over the list, which is repeatingly mapping over the whole term, we map once over the term and perform the substitution of constants there. Most of the time the term is orders of magnitudes bigger than the list, as this function is typically used to force the body of opaque proof terms.
We also introduce a cache internal to this function to only compute the expansion once.
This source of slowdown was observed when calling the checker on compcert.