[stm] fix regression introduced in de2d782 #17743

gares · 2023-06-16T13:32:18Z

Alternative to #17742

The finish API is called both by clients and internally by the STM whenever a VtNow command is executed to obtain the new parsing state. Commit de2d782 makes finish cache the state, which is not a problem if do it once, but may increase memory consumption substantially when checking documents containing many commands classified as VtNow.

SkySkimmer · 2023-06-16T13:52:19Z

@coqbot bench

proux01 · 2023-06-16T13:57:38Z

Successfully tested on order.v in MathComp.
Also successfully tested on the entire MathComp.

gares · 2023-06-16T14:41:29Z

It may be worth backporting to 8.17 if a new point release is to happen, CC @Zimmi48

Zimmi48 · 2023-06-16T16:23:59Z

Sure, I was planning an 8.17.1 release, but this fix is even a good justification in itself to do it.

SkySkimmer · 2023-06-16T22:53:15Z

Do we know why mathcomp is particularly impacted? Are there that much more notations than elsewhere?

coqbot-app · 2023-06-17T05:59:20Z

🏁 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-ssreflect │  244.83   249.17  -1.74 │  1120254288217   1140435585109  -1.77 │  1979942772688   1985863576089  -0.30 │ 2631728  4824940  -45.46 │
│             coq-math-classes │   84.23    85.00  -0.91 │   381632441212    384357096327  -0.71 │   538413626253    538612163154  -0.04 │  516976   518752   -0.34 │
│                 coq-coqprime │   44.88    45.18  -0.66 │   202761256561    203613832305  -0.42 │   311050656321    312154005405  -0.35 │  773496   777128   -0.47 │
│                 coq-compcert │  281.25   282.90  -0.58 │  1275193828627   1283240169632  -0.63 │  1960943233107   1967660797156  -0.34 │ 1133916  1131972    0.17 │
│                 coq-rewriter │  346.61   348.37  -0.51 │  1577869797586   1587392978213  -0.60 │  2623735260445   2626452397836  -0.10 │ 1211584  1214672   -0.25 │
│                    coq-color │  221.12   222.23  -0.50 │   999029093605   1004188230920  -0.51 │  1466004614228   1470213308428  -0.29 │ 1162716  1170844   -0.69 │
│                coq-fourcolor │ 1514.63  1522.08  -0.49 │  6908391692974   6945175226133  -0.53 │ 12502199503928  12510194132866  -0.06 │ 2288984  2291128   -0.09 │
│                     coq-corn │  772.47   776.06  -0.46 │  3517371920226   3533384066926  -0.45 │  5488516042755   5510233353725  -0.39 │  741380   742540   -0.16 │
│               coq-verdi-raft │  553.17   554.94  -0.32 │  2522827218676   2532449931529  -0.38 │  3971035016203   3974722184831  -0.09 │  813296   817528   -0.52 │
│                    coq-verdi │   46.24    46.36  -0.26 │   209291830299    210700891230  -0.67 │   322881216401    323311624896  -0.13 │  526636   526704   -0.01 │
│             coq-fiat-parsers │  323.34   323.95  -0.19 │  1453252964500   1455047991320  -0.12 │  2434682331307   2439603373212  -0.20 │ 2422040  2421772    0.01 │
│                     coq-hott │  147.18   147.43  -0.17 │   665756467191    666217400060  -0.07 │  1057977567847   1059849257330  -0.18 │  621236   623320   -0.33 │
│                  coq-unimath │ 1494.24  1496.68  -0.16 │  6812729929672   6822986281737  -0.15 │ 12822018105610  12845542994824  -0.18 │ 1328712  1332200   -0.26 │
│                  coq-bignums │   27.59    27.63  -0.14 │   125875050386    125857571473   0.01 │   180488939514    180921620755  -0.24 │  483704   488528   -0.99 │
│            coq-iris-examples │  476.56   477.22  -0.14 │  2165501387073   2166490760690  -0.05 │  3325021899487   3341632031746  -0.50 │ 1054700  1076608   -2.03 │
│          coq-category-theory │  711.47   712.20  -0.10 │  3246955830307   3249756558243  -0.09 │  5619407100665   5622303893355  -0.05 │  892956   892216    0.08 │
│        coq-mathcomp-solvable │  147.28   147.43  -0.10 │   672177551466    672700076092  -0.08 │  1085714534394   1087138973736  -0.13 │ 1714168  1723676   -0.55 │
│ coq-fiat-crypto-with-bedrock │ 6073.15  6078.23  -0.08 │ 27592766497922  27613633027840  -0.08 │ 50961476115682  51015767370901  -0.11 │ 2307552  2414604   -4.43 │
│                coq-perennial │ 5868.20  5871.42  -0.05 │ 26768423513202  26780148909348  -0.04 │ 44757293328078  44743345582912   0.03 │ 2218132  2131940    4.04 │
│          coq-metacoq-erasure │  303.37   303.45  -0.03 │  1377525351735   1377751569271  -0.02 │  2191859467042   2195342451748  -0.16 │ 2044756  2050056   -0.26 │
│               coq-coquelicot │   38.06    38.03   0.08 │   170570480809    170641051174  -0.04 │   238804106329    239174972908  -0.16 │  809988   812404   -0.30 │
│   coq-performance-tests-lite │  756.10   755.41   0.09 │  3427250303180   3423251422347   0.12 │  6040749027163   6041569302084  -0.01 │ 1669980  1667780    0.13 │
│            coq-metacoq-pcuic │  617.49   616.09   0.23 │  2805596805803   2798527526164   0.25 │  4151468788290   4156297793284  -0.12 │ 2095952  2095180    0.04 │
│           coq-mathcomp-field │  246.49   245.91   0.24 │  1125557983586   1123263842817   0.20 │  1928642432095   1927944392160   0.04 │ 1431788  1559856   -8.21 │
│      coq-metacoq-safechecker │  373.82   372.89   0.25 │  1709566041440   1705026154300   0.27 │  2850917227247   2852438862239  -0.05 │ 2050780  2051776   -0.05 │
│                coq-fiat-core │   58.64    58.47   0.29 │   251735233484    252321449913  -0.23 │   374097582029    374910198702  -0.22 │  489116   491096   -0.40 │
│  coq-rewriter-perf-SuperFast │  733.36   731.15   0.30 │  3336739570952   3326331199189   0.31 │  5782870388220   5791102659945  -0.14 │ 1311792  1443508   -9.12 │
│                      coq-vst │  853.20   850.57   0.31 │  3878504636596   3866545417985   0.31 │  6365463532185   6383719058530  -0.29 │ 2113864  2116368   -0.12 │
│                  coq-coqutil │   38.54    38.40   0.36 │   173360114540    172673472568   0.40 │   251489172432    251840987475  -0.14 │  558708   558608    0.02 │
│        coq-engine-bench-lite │  156.49   155.85   0.41 │   671335345016    668413702191   0.44 │  1258875298683   1253997825791   0.39 │ 1209456  1324224   -8.67 │
│                 coq-bedrock2 │  312.53   311.25   0.41 │  1426495427510   1420351005800   0.43 │  2803657105151   2806538733070  -0.10 │  833904   836752   -0.34 │
│         coq-metacoq-template │  162.01   161.31   0.43 │   724839766662    721578156374   0.45 │  1154930451140   1156748879422  -0.16 │ 1255040  1261064   -0.48 │
│                     coq-core │  114.14   113.63   0.45 │   474989357041    467034825927   1.70 │   478141578628    478409377254  -0.06 │  291636   290916    0.25 │
│        coq-mathcomp-fingroup │   37.77    37.59   0.48 │   172409128975    171845568135   0.33 │   262139516465    262578989311  -0.17 │  556436   569996   -2.38 │
│                coq-equations │   10.65    10.59   0.57 │    46077392688     46137173470  -0.13 │    73223785426     73311985949  -0.12 │  413228   414720   -0.36 │
│       coq-mathcomp-odd-order │  867.59   862.60   0.58 │  3970327960635   3947385136626   0.58 │  6627781650064   6633245156968  -0.08 │ 1471260  1592680   -7.62 │
│         coq-mathcomp-algebra │  665.37   661.39   0.60 │  3039247731187   3019321732085   0.66 │  5348093281720   5351521945012  -0.06 │ 2056260  4184324  -50.86 │
│                   coq-stdlib │  412.49   409.78   0.66 │  1770426257633   1759856587984   0.60 │  1446584509450   1449133417740  -0.18 │  646952   649140   -0.34 │
│       coq-mathcomp-character │  164.96   163.80   0.71 │   754193176968    748621338435   0.74 │  1170854085251   1172267663616  -0.12 │ 1599100  1732256   -7.69 │
│     coq-metacoq-translations │   17.75    17.54   1.20 │    78984423296     78368581468   0.79 │   128188071739    128263403707  -0.06 │  905520   905792   -0.03 │
└──────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┘

INFO: failed to install
coq-geocoq

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SLOW DOWNS                                                               │
│                                                                                                                                               │
│   OLD       NEW      DIFF    %DIFF     Ln                     FILE                                                                            │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  41.3820   45.6070  4.2250    10.21%  1002  coq-perennial/src/program_proof/simplepb/pb_apply_proof.v.html                                    │
│  31.0840   33.8430  2.7590     8.88%  1730  coq-perennial/src/program_proof/simplepb/simplelog/proof.v.html                                   │
│  21.8120   24.2930  2.4810    11.37%   667  coq-perennial/src/program_proof/simplepb/pb_roapply_proof.v.html                                  │
│  20.4750   22.8750  2.4000    11.72%  1357  coq-perennial/src/program_proof/wal/installer_proof.v.html                                        │
│  45.5530   46.7840  1.2310     2.70%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │
│   5.5400    6.3550  0.8150    14.71%  1391  coq-perennial/src/program_proof/aof/proof.v.html                                                  │
│  80.9060   81.5720  0.6660     0.82%   618  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                       │
│   3.7540    4.3010  0.5470    14.57%     5  coq-mathcomp-algebra/mathcomp/algebra/ssrint.v.html                                               │
│  39.7310   40.2640  0.5330     1.34%   827  coq-vst/veric/binop_lemmas4.v.html                                                                │
│   4.7070    5.1950  0.4880    10.37%  1470  coq-perennial/src/program_proof/simplepb/apps/eesm_proof.v.html                                   │
│  60.9800   61.4270  0.4470     0.73%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                      │
│ 128.6070  128.9930  0.3860     0.30%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                   │
│  27.6350   28.0130  0.3780     1.37%    12  coq-fourcolor/theories/job223to226.v.html                                                         │
│  13.3730   13.7410  0.3680     2.75%   187  coq-perennial/src/goose_lang/interpreter/disk_interpreter.v.html                                  │
│   5.3410    5.7040  0.3630     6.80%   429  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html                                    │
│  42.9060   43.2680  0.3620     0.84%   236  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html         │
│  30.9690   31.3250  0.3560     1.15%   577  coq-perennial/src/program_proof/simplepb/pb_becomeprimary_proof.v.html                            │
│ 128.9970  129.3490  0.3520     0.27%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                   │
│  50.0710   50.4000  0.3290     0.66%   365  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                 │
│   2.9250    3.2490  0.3240    11.08%  1409  coq-perennial/src/program_proof/wal/installer_proof.v.html                                        │
│   2.0560    2.3800  0.3240    15.76%   209  coq-stdlib/setoid_ring/Ncring_tac.v.html                                                          │
│   0.0330    0.3520  0.3190   966.67%   279  coq-perennial/src/program_proof/wal/circ_proof_crash.v.html                                       │
│   0.0300    0.3390  0.3090  1030.00%   509  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v.html            │
│   1.2670    1.5620  0.2950    23.28%  1874  coq-perennial/src/program_proof/wal/recovery_proof.v.html                                         │
│   0.5270    0.8080  0.2810    53.32%   422  coq-stdlib/MSets/MSetList.v.html                                                                  │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                     TOP 25 SPEED UPS                                                      │
│                                                                                                                           │
│   OLD       NEW      DIFF     %DIFF    Ln                 FILE                                                            │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  59.8310   58.8770  -0.9540   -1.59%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html      │
│ 142.3870  141.5810  -0.8060   -0.57%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │
│  25.8210   25.0990  -0.7220   -2.80%  2293  coq-perennial/src/goose_lang/logical_reln_fund.v.html                         │
│  29.8430   29.1830  -0.6600   -2.21%    12  coq-fourcolor/theories/job287to290.v.html                                     │
│  17.2040   16.5760  -0.6280   -3.65%  3269  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html           │
│   3.2940    2.7580  -0.5360  -16.27%   487  coq-stdlib/Numbers/HexadecimalFacts.v.html                                    │
│  27.5300   27.0300  -0.5000   -1.82%    12  coq-fourcolor/theories/job227to230.v.html                                     │
│  52.0230   51.5940  -0.4290   -0.82%   915  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html     │
│  24.5460   24.1180  -0.4280   -1.74%    12  coq-fourcolor/theories/job384to398.v.html                                     │
│   9.1290    8.7040  -0.4250   -4.66%  1508  coq-perennial/src/program_proof/wal/recovery_proof.v.html                     │
│  43.0380   42.6160  -0.4220   -0.98%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html    │
│   4.5600    4.1560  -0.4040   -8.86%  1388  coq-perennial/src/program_proof/simplepb/apps/eesm_proof.v.html               │
│   1.5200    1.1160  -0.4040  -26.58%   587  coq-metacoq-erasure/erasure/theories/ErasureFunction.v.html                   │
│  20.2820   19.8910  -0.3910   -1.93%    12  coq-fourcolor/theories/job271to278.v.html                                     │
│  33.7230   33.3610  -0.3620   -1.07%    12  coq-fourcolor/theories/job001to106.v.html                                     │
│  31.4980   31.1390  -0.3590   -1.14%    12  coq-fourcolor/theories/job563to588.v.html                                     │
│  22.9470   22.6000  -0.3470   -1.51%    12  coq-fourcolor/theories/job307to310.v.html                                     │
│  27.1980   26.8660  -0.3320   -1.22%    12  coq-fourcolor/theories/job299to302.v.html                                     │
│   5.2730    4.9470  -0.3260   -6.18%   747  coq-perennial/src/program_proof/fencing/frontend_proof.v.html                 │
│   0.3740    0.0490  -0.3250  -86.90%  1447  coq-perennial/src/program_proof/aof/proof.v.html                              │
│  29.6800   29.3690  -0.3110   -1.05%    12  coq-fourcolor/theories/job399to438.v.html                                     │
│   1.2140    0.9040  -0.3100  -25.54%   202  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/BaseConversion.v.html    │
│   5.9470    5.6450  -0.3020   -5.08%   167  coq-vst/veric/binop_lemmas6.v.html                                            │
│  27.6800   27.3860  -0.2940   -1.06%    12  coq-fourcolor/theories/job499to502.v.html                                     │
│   0.5980    0.3050  -0.2930  -49.00%   233  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReduction.v.html  │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

proux01 · 2023-06-17T09:56:03Z

Do we know why mathcomp is particularly impacted? Are there that much more notations than elsewhere?

It's obviously linked to hierarchy-builder since the affected files are the heavy users of HB but I don't have a better understanding (note that even with the patch, those files remain memory heavy).

proux01 · 2023-06-17T09:56:12Z

@coqbot run full ci

gares · 2023-06-17T13:11:20Z

Do we know why mathcomp is particularly impacted? Are there that much more notations than elsewhere?

Elpi commands can import a module, so for now they are declared as VtNow.

proux01 · 2023-06-17T16:48:42Z

Bench is good, CI failures are unrelated, let's merge.

@coqbot merge now

coqbot-app · 2023-06-17T16:48:44Z

@proux01: You can't merge the PR because it hasn't been approved yet.

proux01 · 2023-06-17T16:49:08Z

@coqbot merge now

Zimmi48 · 2023-06-19T13:53:42Z

Unfortunately, a naive backport of this PR doesn't produce code that builds, probably due to #17059, which also creates difficulties for backporting #17620. This creates the question whether backporting #17059 too would be worthwhile. Unfortunately, it changes quite a few signatures in the API of the STM. I don't know if these functions should be considered internal.

SkySkimmer · 2023-06-19T14:01:07Z

This creates the question whether backporting #17059 too would be worthwhile

It's not

SkySkimmer · 2023-06-19T14:07:46Z

stm/stm.ml

@@ -2695,7 +2695,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) x c =
            begin match w with
              | VtNow ->
                (* We need to execute to get the new parsing state *)
-                ignore(finish ~doc:dummy_doc);
+                let () = observe ~doc:dummy_doc (VCS.get_branch_pos (VCS.current_branch ())) in


ignore (observe ...) should work for the backport

gares added the kind: fix This fixes a bug or incorrect documentation. label Jun 16, 2023

gares added this to the 8.18+rc1 milestone Jun 16, 2023

gares requested a review from a team as a code owner June 16, 2023 13:32

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 16, 2023

gares mentioned this pull request Jun 16, 2023

Fix memory issue with MathComp 2 #17742

Closed

6 tasks

proux01 added part: STM State Transition Machine, asynchronous proofs, etc. kind: performance Improvements to performance and efficiency. labels Jun 16, 2023

Zimmi48 modified the milestones: 8.18+rc1, 8.17.1 Jun 16, 2023

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 17, 2023

proux01 self-assigned this Jun 17, 2023

proux01 approved these changes Jun 17, 2023

View reviewed changes

coqbot-app bot merged commit 933c7c3 into coq:master Jun 17, 2023
6 of 9 checks passed

coqbot-app bot added this to Request 8.17.1 inclusion in Coq 8.17 Jun 17, 2023

gares deleted the fix-memory-leak branch June 17, 2023 20:23

Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Jun 19, 2023

Backport PR coq#17743: [stm] fix regression introduced in de2d782

f3df7a5

SkySkimmer reviewed Jun 19, 2023

View reviewed changes

Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Jun 20, 2023

Backport PR coq#17743: [stm] fix regression introduced in de2d782

c716867

coqbot-app bot moved this from Request 8.17.1 inclusion to Shipped in 8.17.1 in Coq 8.17 Jun 21, 2023

Zimmi48 mentioned this pull request Jun 22, 2023

Changelog for 8.17.1. #17762

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[stm] fix regression introduced in de2d782 #17743

[stm] fix regression introduced in de2d782 #17743

gares commented Jun 16, 2023

SkySkimmer commented Jun 16, 2023

proux01 commented Jun 16, 2023 •

edited

gares commented Jun 16, 2023

Zimmi48 commented Jun 16, 2023

SkySkimmer commented Jun 16, 2023

coqbot-app bot commented Jun 17, 2023

proux01 commented Jun 17, 2023 •

edited

proux01 commented Jun 17, 2023

gares commented Jun 17, 2023

proux01 commented Jun 17, 2023

coqbot-app bot commented Jun 17, 2023

proux01 commented Jun 17, 2023

Zimmi48 commented Jun 19, 2023

SkySkimmer commented Jun 19, 2023

SkySkimmer Jun 19, 2023

[stm] fix regression introduced in de2d782 #17743

[stm] fix regression introduced in de2d782 #17743

Conversation

gares commented Jun 16, 2023

SkySkimmer commented Jun 16, 2023

proux01 commented Jun 16, 2023 • edited

gares commented Jun 16, 2023

Zimmi48 commented Jun 16, 2023

SkySkimmer commented Jun 16, 2023

coqbot-app bot commented Jun 17, 2023

proux01 commented Jun 17, 2023 • edited

proux01 commented Jun 17, 2023

gares commented Jun 17, 2023

proux01 commented Jun 17, 2023

coqbot-app bot commented Jun 17, 2023

proux01 commented Jun 17, 2023

Zimmi48 commented Jun 19, 2023

SkySkimmer commented Jun 19, 2023

SkySkimmer Jun 19, 2023

Choose a reason for hiding this comment

proux01 commented Jun 16, 2023 •

edited

proux01 commented Jun 17, 2023 •

edited