| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Based on https://github.com/coq/coq/issues/8993#issuecomment-438572277,
I am guessing that DCE is currently memory-hungry. This makes sense,
because every [var] is carrying around a full `PositiveSet.t` when
computing live variables. Instead, we now adjust `subst01` to not
increment counts coming from dead variables, and use it to implement
DCE. Hopefully this will be much faster and more efficient.
N.B. It was important to stop doing union of `PositiveMap.t`, and
instead add to them incrementally.
Before: p384_32.c (real: 406.78, user: 391.99, sys: 14.82, mem: 16896040 ko)
After: p384_32.c (real: 201.11, user: 200.33, sys: 0.80, mem: 1039520 ko)
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------------------------------
21m16.47s | Total | 24m45.69s || -3m29.22s | -14.08%
--------------------------------------------------------------------------------------------------------------------
3m20.33s | p384_32.c | 6m31.99s || -3m11.66s | -48.89%
0m14.08s | secp256k1_32.c | 0m18.85s || -0m04.77s | -25.30%
0m13.86s | p256_32.c | 0m18.14s || -0m04.28s | -23.59%
6m14.92s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m17.66s || -0m02.74s | -0.72%
4m37.51s | Experiments/NewPipeline/Toplevel1.vo | 4m39.20s || -0m01.68s | -0.60%
0m06.46s | p224_32.c | 0m07.85s || -0m01.38s | -17.70%
0m02.49s | Experiments/NewPipeline/MiscCompilerPassesProofs.vo | 0m03.85s || -0m01.35s | -35.32%
1m32.10s | Experiments/NewPipeline/Toplevel2.vo | 1m31.75s || +0m00.34s | +0.38%
0m42.06s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m42.17s || -0m00.10s | -0.26%
0m39.54s | p521_32.c | 0m39.37s || +0m00.17s | +0.43%
0m39.45s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m39.51s || -0m00.05s | -0.15%
0m32.87s | p521_64.c | 0m32.94s || -0m00.07s | -0.21%
0m25.29s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m25.26s || +0m00.02s | +0.11%
0m23.06s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m23.20s || -0m00.14s | -0.60%
0m18.73s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m19.01s || -0m00.28s | -1.47%
0m14.93s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m15.04s || -0m00.10s | -0.73%
0m10.58s | p384_64.c | 0m11.21s || -0m00.63s | -5.61%
0m09.12s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m08.90s || +0m00.21s | +2.47%
0m05.94s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.06s || -0m00.11s | -1.98%
0m05.78s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.76s || +0m00.02s | +0.34%
0m04.36s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.37s || -0m00.00s | -0.22%
0m04.23s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.24s || -0m00.00s | -0.23%
0m03.47s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.68s || -0m00.20s | -5.70%
0m02.38s | curve25519_32.c | 0m02.39s || -0m00.01s | -0.41%
0m02.04s | secp256k1_64.c | 0m02.09s || -0m00.04s | -2.39%
0m01.94s | p224_64.c | 0m01.96s || -0m00.02s | -1.02%
0m01.90s | p256_64.c | 0m01.96s || -0m00.06s | -3.06%
0m01.52s | curve25519_64.c | 0m01.60s || -0m00.08s | -5.00%
0m01.47s | Experiments/NewPipeline/CLI.vo | 0m01.44s || +0m00.03s | +2.08%
0m01.22s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.26s || -0m00.04s | -3.17%
0m01.21s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.27s || -0m00.06s | -4.72%
0m00.97s | Experiments/NewPipeline/CompilersTestCases.vo | 0m01.10s || -0m00.13s | -11.81%
0m00.66s | Experiments/NewPipeline/MiscCompilerPasses.vo | 0m00.62s || +0m00.04s | +6.45%
|
Jason Gross
Jason Gross