experiment: measure gc time with ocaml 5 runtime events in newprofile #18972
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
coqbot-app
bot
added
the
needs: full CI
SkySkimmer
added
the
needs: progress
SkySkimmer
commented
Apr 23, 2024
lib/newProfile.ml
Outdated
| | _ -> () | ||
| in | ||
| let runtime_end _ ts = function | ||
| | EV_MINOR -> begin match !current_minor with |
There was a problem hiding this comment.
the events in runtime_events.mli are not documented so it's not fully clear to what extent this captures minor gc time
also not sure we can really have imbricated events so maybe we don't need the current_minor adhoc stack
SkySkimmer
force-pushed
the
newprof-gc-timing
branch
from
cbb8e7a
to
c9678b5
Compare
|
Testing on List.v, it seems to work but there are some weird instances where gc time is reported while Gc.quick_stat does not report a collection. Not sure what that means. |
SkySkimmer
commented
Apr 24, 2024
|
Seems to work pretty well, here is an example output on List.v (zoomed in on the biggest GC) (for some reason quick_stat reports 1 major collection but we see 2 pairs of begin/end EV_MAJOR) |
SkySkimmer
commented
Apr 26, 2024
| | EV_MAJOR -> | ||
| update Counters.current_major_time current_major ts; | ||
| duration ~is_gc:true ~time:(to_time ts) "gc_major" "E" () | ||
| | _ -> () |
There was a problem hiding this comment.
NB: We could print for every event type but it doesn't seem particularly useful.
|
🏁 Bench results: INFO: failed to install coq-mathcomp-fingroup (dependency coq-mathcomp-ssreflect failed) 🐢 Top 25 slow downs┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 18.1050 27.4550 9.3500 51.64% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 10.8300 19.2500 8.4200 77.75% 496 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html │ │ 11.0470 19.4330 8.3860 75.91% 496 coq-rewriter/src/Rewriter/Rewriter/Wf.v.html │ │ 8.0050 12.5990 4.5940 57.39% 30 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 15.5650 19.6870 4.1220 26.48% 1382 coq-rewriter-perf-SuperFast/src/Rewriter/Language/Wf.v.html │ │ 15.6540 19.5900 3.9360 25.14% 1382 coq-rewriter/src/Rewriter/Language/Wf.v.html │ │ 11.9560 15.4710 3.5150 29.40% 410 coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html │ │ 8.5150 11.0670 2.5520 29.97% 1265 coq-verdi-raft/theories/Raft/CommonTheorems.v.html │ │ 8.0390 10.5740 2.5350 31.53% 356 coq-rewriter/src/Rewriter/Rewriter/Wf.v.html │ │ 8.0360 10.5050 2.4690 30.72% 356 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html │ │ 30.5760 32.9020 2.3260 7.61% 79 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │ │ 30.5930 32.8690 2.2760 7.44% 79 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │ │ 3.6050 5.8670 2.2620 62.75% 29 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 16.7880 18.8100 2.0220 12.04% 61 coq-rewriter/src/Rewriter/Rewriter/Examples/PrefixSums.v.html │ │ 4.2840 6.1670 1.8830 43.95% 166 coq-verdi-raft/theories/RaftProofs/LeaderSublogProof.v.html │ │ 2.5140 4.0840 1.5700 62.45% 62 coq-coqutil/test/SlowGoals.v.html │ │ 4.7580 6.1600 1.4020 29.47% 170 coq-verdi-raft/theories/RaftProofs/LeaderSublogProof.v.html │ │ 5.2090 6.6060 1.3970 26.82% 204 coq-verdi-raft/theories/RaftProofs/LeaderSublogProof.v.html │ │ 12.7150 14.1030 1.3880 10.92% 82 coq-rewriter/src/Rewriter/Rewriter/Examples.v.html │ │ 11.9600 13.2970 1.3370 11.18% 88 coq-rewriter/src/Rewriter/Rewriter/Examples.v.html │ │ 10.1610 11.4950 1.3340 13.13% 978 coq-verdi-raft/theories/Raft/Linearizability.v.html │ │ 3.2590 4.5780 1.3190 40.47% 597 coq-verdi-raft/theories/RaftProofs/AllEntriesLogProof.v.html │ │ 3.0060 4.3170 1.3110 43.61% 654 coq-verdi-raft/theories/Raft/RefinementSpecLemmas.v.html │ │ 9.9570 11.2100 1.2530 12.58% 79 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 4.8810 6.1220 1.2410 25.43% 73 coq-color/Util/Multiset/MultisetList.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 2.1340 1.5400 -0.5940 -27.84% 196 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 8.2500 7.8040 -0.4460 -5.41% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 0.9310 0.6220 -0.3090 -33.19% 198 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 9.9440 9.6950 -0.2490 -2.50% 87 coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html │ │ 19.7320 19.4850 -0.2470 -1.25% 196 coq-unimath/UniMath/HomologicalAlgebra/KATriangulated.v.html │ │ 0.5500 0.3680 -0.1820 -33.09% 11 coq-stdlib/Reals/Alembert.v.html │ │ 13.6920 13.5130 -0.1790 -1.31% 99 coq-unimath/UniMath/HomologicalAlgebra/KATriangulated.v.html │ │ 2.6660 2.4980 -0.1680 -6.30% 490 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 0.5390 0.3790 -0.1600 -29.68% 16 coq-stdlib/Numbers/HexadecimalZ.v.html │ │ 1.6890 1.5360 -0.1530 -9.06% 596 coq-stdlib/Strings/Byte.v.html │ │ 7.3700 7.2240 -0.1460 -1.98% 279 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 0.2680 0.1230 -0.1450 -54.10% 3 coq-fiat-parsers/src/Parsers/ExtrOcamlParsers.v.html │ │ 4.7140 4.5700 -0.1440 -3.05% 128 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 0.3750 0.2330 -0.1420 -37.87% 18 coq-stdlib/micromega/VarMap.v.html │ │ 0.5560 0.4160 -0.1400 -25.18% 16 coq-stdlib/Numbers/DecimalZ.v.html │ │ 0.2910 0.1530 -0.1380 -47.42% 2039 coq-stdlib/FSets/FMapAVL.v.html │ │ 1.3020 1.1760 -0.1260 -9.68% 755 coq-fiat-parsers/src/Parsers/GenericRecognizerOptimized.v.html │ │ 0.6650 0.5400 -0.1250 -18.80% 14 coq-stdlib/MSets/MSetToFiniteSet.v.html │ │ 0.3240 0.2000 -0.1240 -38.27% 138 coq-stdlib/Numbers/HexadecimalPos.v.html │ │ 0.2080 0.0880 -0.1200 -57.69% 7 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/AllTactics.v.html │ │ 39.7570 39.6460 -0.1110 -0.28% 236 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 0.2500 0.1440 -0.1060 -42.40% 1846 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.3120 0.2080 -0.1040 -33.33% 11 coq-stdlib/setoid_ring/Field_theory.v.html │ │ 0.1040 0.0000 -0.1040 -100.00% 47 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html │ │ 0.1040 0.0000 -0.1040 -100.00% 60 coq-rewriter/src/Rewriter/Rewriter/ProofsCommon.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
|
https://coq.gitlabpages.inria.fr/-/coq/-/jobs/4283231/artifacts/_bench/html/coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html has relatively a lot more events printed with this PR (66 -> 2570) but the absolute number doesn't justify total time going 32s -> 50s. Is it just the cost of having runtime_events enabled? |
|
small bench testing without actually calling the poll function https://gitlab.inria.fr/coq/coq/-/jobs/4292164 |
SkySkimmer
force-pushed
the
newprof-gc-timing
branch
2 times, most recently
from
43c6d63
to
322b6b2
Compare
|
@coqbot bench |
|
🏁 Bench results: 🐢 Top 25 slow downs┌───────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.4380 0.7190 0.2810 64.16% 14 coq-stdlib/MSets/MSetToFiniteSet.v.html │ │ 0.3280 0.5640 0.2360 71.95% 1 coq-stdlib/micromega/ZifySint63.v.html │ │ 0.3650 0.5800 0.2150 58.90% 705 coq-stdlib/Numbers/HexadecimalFacts.v.html │ │ 0.3940 0.5950 0.2010 51.02% 16 coq-stdlib/Numbers/DecimalQ.v.html │ │ 0.2690 0.4650 0.1960 72.86% 13 coq-stdlib/extraction/ExtrOCamlInt63.v.html │ │ 0.3680 0.5490 0.1810 49.18% 11 coq-stdlib/QArith/Qpower.v.html │ │ 0.5660 0.7460 0.1800 31.80% 816 coq-stdlib/MSets/MSetRBT.v.html │ │ 0.3310 0.5100 0.1790 54.08% 19 coq-stdlib/Reals/Abstract/ConstructiveLUB.v.html │ │ 0.3490 0.5100 0.1610 46.13% 14 coq-stdlib/Numbers/Cyclic/Abstract/NZCyclic.v.html │ │ 0.2880 0.4380 0.1500 52.08% 31 coq-stdlib/Reals/Abstract/ConstructiveRealsMorphisms.v.html │ │ 0.2080 0.3410 0.1330 63.94% 219 coq-stdlib/Reals/Abstract/ConstructiveMinMax.v.html │ │ 3.0900 3.2080 0.1180 3.82% 487 coq-stdlib/Numbers/HexadecimalFacts.v.html │ │ 0.2140 0.3210 0.1070 50.00% 11 coq-stdlib/setoid_ring/Field_theory.v.html │ │ 0.3540 0.4560 0.1020 28.81% 1364 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.3300 0.4280 0.0980 29.70% 12 coq-stdlib/MSets/MSets.v.html │ │ 0.2010 0.2970 0.0960 47.76% 652 coq-stdlib/ZArith/Znumtheory.v.html │ │ 0.1500 0.2410 0.0910 60.67% 1131 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.2790 0.3690 0.0900 32.26% 20 coq-stdlib/FSets/FSetDecide.v.html │ │ 1.1980 1.2860 0.0880 7.35% 854 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.2580 0.3460 0.0880 34.11% 650 coq-stdlib/MSets/MSetRBT.v.html │ │ 0.2880 0.3700 0.0820 28.47% 12 coq-stdlib/Reals/Abstract/ConstructiveMinMax.v.html │ │ 0.2290 0.3070 0.0780 34.06% 778 coq-stdlib/setoid_ring/Ring_polynom.v.html │ │ 0.1270 0.2050 0.0780 61.42% 681 coq-stdlib/Numbers/HexadecimalFacts.v.html │ │ 8.5350 8.6120 0.0770 0.90% 1265 coq-verdi-raft/theories/Raft/CommonTheorems.v.html │ │ 2.2190 2.2960 0.0770 3.47% 657 coq-verdi-raft/theories/Raft/RefinementSpecLemmas.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 2.1480 1.6340 -0.5140 -23.93% 196 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 1.0910 0.7510 -0.3400 -31.16% 813 coq-stdlib/MSets/MSetRBT.v.html │ │ 0.8110 0.4720 -0.3390 -41.80% 200 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 0.9570 0.6910 -0.2660 -27.80% 198 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 18.4370 18.1740 -0.2630 -1.43% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 9.9600 9.7190 -0.2410 -2.42% 87 coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html │ │ 12.0400 11.8020 -0.2380 -1.98% 410 coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html │ │ 1.1860 0.9720 -0.2140 -18.04% 384 coq-stdlib/MSets/MSetAVL.v.html │ │ 0.6850 0.4920 -0.1930 -28.18% 2108 coq-stdlib/FSets/FMapFacts.v.html │ │ 0.3480 0.1610 -0.1870 -53.74% 744 coq-stdlib/MSets/MSetAVL.v.html │ │ 17.9920 17.8070 -0.1850 -1.03% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 4.8060 4.6300 -0.1760 -3.66% 170 coq-verdi-raft/theories/RaftProofs/LeaderSublogProof.v.html │ │ 0.5510 0.3780 -0.1730 -31.40% 16 coq-stdlib/Numbers/DecimalN.v.html │ │ 0.3000 0.1280 -0.1720 -57.33% 578 coq-stdlib/Reals/Abstract/ConstructiveMinMax.v.html │ │ 0.5520 0.3840 -0.1680 -30.43% 17 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 0.4410 0.2990 -0.1420 -32.20% 19 coq-stdlib/Sorting/Heap.v.html │ │ 0.3790 0.2410 -0.1380 -36.41% 20 coq-stdlib/MSets/MSetDecide.v.html │ │ 0.4310 0.3040 -0.1270 -29.47% 16 coq-stdlib/Numbers/HexadecimalZ.v.html │ │ 0.3200 0.2020 -0.1180 -36.87% 11 coq-stdlib/setoid_ring/Field.v.html │ │ 5.2700 5.1550 -0.1150 -2.18% 204 coq-verdi-raft/theories/RaftProofs/LeaderSublogProof.v.html │ │ 15.5990 15.4910 -0.1080 -0.69% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 0.4040 0.2970 -0.1070 -26.49% 14 coq-stdlib/FSets/FSetToFiniteSet.v.html │ │ 0.5610 0.4550 -0.1060 -18.89% 11 coq-stdlib/setoid_ring/Integral_domain.v.html │ │ 0.7040 0.5980 -0.1060 -15.06% 2224 coq-stdlib/FSets/FMapAVL.v.html │ │ 8.1140 8.0090 -0.1050 -1.29% 30 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
SkySkimmer
force-pushed
the
newprof-gc-timing
branch
from
b81c0c9
to
0c14c15
Compare
|
🏁 Bench results: 🐢 Top 25 slow downs┌──────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 1.6150 1.8950 0.2800 17.34% 596 coq-stdlib/Strings/Byte.v.html │ │ 2.7740 3.0010 0.2270 8.18% 122 coq-stdlib/setoid_ring/Ncring_initial.v.html │ │ 0.9000 1.1120 0.2120 23.56% 854 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.3870 0.5990 0.2120 54.78% 17 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 0.3080 0.5080 0.2000 64.94% 1364 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.3240 0.4930 0.1690 52.16% 16 coq-stdlib/Numbers/DecimalNat.v.html │ │ 0.4280 0.5930 0.1650 38.55% 16 coq-stdlib/Numbers/DecimalZ.v.html │ │ 0.2940 0.4520 0.1580 53.74% 861 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.4450 0.5960 0.1510 33.93% 16 coq-stdlib/Numbers/DecimalQ.v.html │ │ 0.4100 0.5600 0.1500 36.59% 11 coq-stdlib/QArith/Qpower.v.html │ │ 0.3280 0.4740 0.1460 44.51% 19 coq-stdlib/Reals/Abstract/ConstructiveLUB.v.html │ │ 0.3590 0.5040 0.1450 40.39% 16 coq-stdlib/Numbers/Cyclic/Int63/Cyclic63.v.html │ │ 0.1710 0.3140 0.1430 83.63% 744 coq-stdlib/MSets/MSetAVL.v.html │ │ 0.2390 0.3650 0.1260 52.72% 11 coq-stdlib/omega/OmegaLemmas.v.html │ │ 0.2820 0.3960 0.1140 40.43% 877 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.2110 0.3240 0.1130 53.55% 11 coq-stdlib/setoid_ring/Field_theory.v.html │ │ 3.4610 3.5730 0.1120 3.24% 490 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 0.2220 0.3310 0.1090 49.10% 11 coq-stdlib/ZArith/Wf_Z.v.html │ │ 0.1270 0.2340 0.1070 84.25% 760 coq-stdlib/setoid_ring/Ring_polynom.v.html │ │ 0.4150 0.5200 0.1050 25.30% 19 coq-stdlib/FSets/FSetFacts.v.html │ │ 0.2190 0.3220 0.1030 47.03% 11 coq-stdlib/ZArith/Zbool.v.html │ │ 0.1660 0.2670 0.1010 60.84% 863 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.3690 0.4700 0.1010 27.37% 13 coq-stdlib/ZArith/Zmax.v.html │ │ 1.5510 1.6490 0.0980 6.32% 583 coq-stdlib/Strings/Byte.v.html │ │ 0.2310 0.3250 0.0940 40.69% 11 coq-stdlib/setoid_ring/ZArithRing.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 2.2110 1.6640 -0.5470 -24.74% 196 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 18.5020 18.1740 -0.3280 -1.77% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 0.9950 0.7550 -0.2400 -24.12% 467 coq-stdlib/Numbers/DecimalFacts.v.html │ │ 0.9120 0.6760 -0.2360 -25.88% 198 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 1.4270 1.2160 -0.2110 -14.79% 316 coq-stdlib/Strings/Byte.v.html │ │ 2.0240 1.8280 -0.1960 -9.68% 25 coq-engine-bench-lite/coq/PerformanceDemos/app_n.v.html │ │ 0.5830 0.3870 -0.1960 -33.62% 11 coq-stdlib/setoid_ring/Integral_domain.v.html │ │ 0.3650 0.1740 -0.1910 -52.33% 2222 coq-stdlib/FSets/FMapAVL.v.html │ │ 9.9260 9.7460 -0.1800 -1.81% 87 coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html │ │ 15.2830 15.1160 -0.1670 -1.09% 325 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 0.8170 0.6550 -0.1620 -19.83% 170 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 0.3540 0.2020 -0.1520 -42.94% 1627 coq-stdlib/Numbers/Cyclic/Int63/Uint63.v.html │ │ 0.3220 0.1710 -0.1510 -46.89% 2039 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.5230 0.3760 -0.1470 -28.11% 16 coq-stdlib/Numbers/DecimalN.v.html │ │ 0.4040 0.2590 -0.1450 -35.89% 15 coq-stdlib/QArith/Qcabs.v.html │ │ 8.1500 8.0130 -0.1370 -1.68% 30 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 15.4420 15.3070 -0.1350 -0.87% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 0.3920 0.2690 -0.1230 -31.38% 11 coq-stdlib/QArith/QArith.v.html │ │ 0.2720 0.1500 -0.1220 -44.85% 1846 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.3780 0.2560 -0.1220 -32.28% 17 coq-stdlib/micromega/Lqa.v.html │ │ 0.4710 0.3550 -0.1160 -24.63% 13 coq-stdlib/extraction/ExtrOCamlPArray.v.html │ │ 0.6900 0.5820 -0.1080 -15.65% 2224 coq-stdlib/FSets/FMapAVL.v.html │ │ 0.3940 0.2890 -0.1050 -26.65% 14 coq-stdlib/FSets/FSetToFiniteSet.v.html │ │ 5.8760 5.7730 -0.1030 -1.75% 109 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 1.2040 1.1050 -0.0990 -8.22% 21 coq-engine-bench-lite/coq/PerformanceDemos/app_n.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
|
Looks like the first attempt was polling too often. The engine-bench pattern file has over 10 million unification calls, I guess 10 million polls = 20 extra seconds (2us / poll, mostly empty polls)? |
|
🏁 Bench results: INFO: failed to install coq-mathcomp-fingroup (dependency coq-mathcomp-ssreflect failed) 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 44.1450 44.4500 0.3050 0.69% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 17.9960 18.2750 0.2790 1.55% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 0.3990 0.6390 0.2400 60.15% 16 coq-stdlib/Numbers/DecimalZ.v.html │ │ 0.5250 0.7620 0.2370 45.14% 422 coq-stdlib/MSets/MSetList.v.html │ │ 0.3540 0.5630 0.2090 59.04% 868 coq-stdlib/MSets/MSetRBT.v.html │ │ 0.3690 0.5660 0.1970 53.39% 11 coq-stdlib/Reals/Binomial.v.html │ │ 0.4680 0.6510 0.1830 39.10% 11 coq-stdlib/setoid_ring/Rings_Z.v.html │ │ 0.3200 0.4940 0.1740 54.37% 16 coq-stdlib/Numbers/DecimalNat.v.html │ │ 0.2710 0.4400 0.1690 62.36% 12 coq-stdlib/Reals/Abstract/ConstructiveMinMax.v.html │ │ 0.3390 0.4990 0.1600 47.20% 19 coq-stdlib/Reals/Abstract/ConstructiveLUB.v.html │ │ 9.1170 9.2610 0.1440 1.58% 673 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html │ │ 0.6800 0.8210 0.1410 20.74% 813 coq-stdlib/MSets/MSetRBT.v.html │ │ 0.2730 0.4100 0.1370 50.18% 13 coq-stdlib/FSets/FSetCompat.v.html │ │ 0.2300 0.3520 0.1220 53.04% 313 coq-stdlib/Reals/Abstract/ConstructiveLUB.v.html │ │ 0.3790 0.4980 0.1190 31.40% 11 coq-stdlib/QArith/Qpower.v.html │ │ 0.0000 0.1160 0.1160 inf% 60 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/ProofsCommon.v.html │ │ 18.3760 18.4920 0.1160 0.63% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 10.9460 11.0620 0.1160 1.06% 496 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html │ │ 12.6370 12.7520 0.1150 0.91% 1408 coq-rewriter-perf-SuperFast/src/Rewriter/Language/Wf.v.html │ │ 0.4190 0.5330 0.1140 27.21% 17 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 0.0000 0.1120 0.1120 inf% 51 coq-rewriter/src/Rewriter/Rewriter/Wf.v.html │ │ 0.0000 0.1110 0.1110 inf% 63 coq-rewriter/src/Rewriter/Rewriter/ProofsCommon.v.html │ │ 0.0010 0.1120 0.1110 11100.00% 54 coq-rewriter/src/Rewriter/Rewriter/ProofsCommonTactics.v.html │ │ 0.0000 0.1110 0.1110 inf% 50 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html │ │ 0.0000 0.1110 0.1110 inf% 53 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/ProofsCommonTactics.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 3.2310 2.2400 -0.9910 -30.67% 487 coq-stdlib/Numbers/HexadecimalFacts.v.html │ │ 10.2130 9.8800 -0.3330 -3.26% 87 coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html │ │ 2.9940 2.6810 -0.3130 -10.45% 208 coq-verdi-raft/theories/RaftProofs/LeaderSublogProof.v.html │ │ 16.9400 16.7070 -0.2330 -1.38% 61 coq-rewriter/src/Rewriter/Rewriter/Examples/PrefixSums.v.html │ │ 0.5940 0.3690 -0.2250 -37.88% 11 coq-stdlib/Reals/Abstract/ConstructivePower.v.html │ │ 0.6080 0.4010 -0.2070 -34.05% 11 coq-stdlib/Floats/FloatAxioms.v.html │ │ 0.5610 0.3700 -0.1910 -34.05% 11 coq-stdlib/Reals/Alembert.v.html │ │ 4.7570 4.5660 -0.1910 -4.02% 128 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 0.6060 0.4170 -0.1890 -31.19% 11 coq-stdlib/Numbers/Cyclic/Int63/Sint63.v.html │ │ 0.5320 0.3470 -0.1850 -34.77% 1 coq-stdlib/micromega/ZifySint63.v.html │ │ 0.5340 0.3620 -0.1720 -32.21% 705 coq-stdlib/Numbers/HexadecimalFacts.v.html │ │ 5.6240 5.4520 -0.1720 -3.06% 178 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/InterpProofs.v.html │ │ 0.6250 0.4560 -0.1690 -27.04% 200 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 12.1160 11.9490 -0.1670 -1.38% 88 coq-rewriter/src/Rewriter/Rewriter/Examples.v.html │ │ 1.3740 1.2080 -0.1660 -12.08% 167 coq-hott/theories/Spaces/Torus/TorusEquivCircles.v.html │ │ 7.7220 7.5660 -0.1560 -2.02% 27 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v.html │ │ 3.0220 2.8680 -0.1540 -5.10% 122 coq-stdlib/setoid_ring/Ncring_initial.v.html │ │ 3.4250 3.2780 -0.1470 -4.29% 174 coq-verdi-raft/theories/RaftProofs/LeaderSublogProof.v.html │ │ 15.8060 15.6600 -0.1460 -0.92% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 1.3200 1.1750 -0.1450 -10.98% 755 coq-fiat-parsers/src/Parsers/GenericRecognizerOptimized.v.html │ │ 5.0590 4.9160 -0.1430 -2.83% 73 coq-color/Util/Multiset/MultisetList.v.html │ │ 0.4100 0.2730 -0.1370 -33.41% 15 coq-stdlib/QArith/Qcabs.v.html │ │ 4.4810 4.3440 -0.1370 -3.06% 571 coq-verdi-raft/theories/Raft/CommonTheorems.v.html │ │ 0.2620 0.1260 -0.1360 -51.91% 3 coq-fiat-parsers/src/Parsers/ExtrOcamlParsers.v.html │ │ 6.5060 6.3720 -0.1340 -2.06% 308 coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
github-actions
bot
added
the
needs: rebase
They are on a separate thread as google trace format requires well bracketing of events in a given thread. Not sure if ocaml 5 does GC in parallel with our main thread, it seems plausible.
SkySkimmer
force-pushed
the
newprof-gc-timing
branch
from
0c14c15
to
9e8a057
Compare
coqbot-app
bot
removed
the
needs: rebase
github-actions
bot
added
the
needs: rebase
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.