| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Andres and I met today, and discovered that there's a source of
non-linear complexity in the rewriter which is not type casts.
In adding side-conditions to the rewrite rules (which are not discussed
in the pattern-matching compilation paper), I represented them by
allowing rewrite rules to fail. So, for example,
# + x ~~> x (when # == 0)
is represented as
# + x ~~> if (# =? 0) then Some x else None
In the case that a rewrite rule fails, we need to try all other rewrite
rules that might still apply. However, doing this in the naive-CPS way
leads to non-linear blowup, because wildcard rewrite rules get
duplicated in the failure branches. (This is similar to the issue that
`match x with "some string" => true | _ => false end%string` will
generate a large number of "false" branches, and duplicate "false"
across all of them, rather than having a single default case.)
For example, if we had the rewrite rules
# + # ~~> literal sum
x + (-y) ~~> x - y
(-x) + y ~~> y - x
then the compiled code would look like
fun x y
=> if x is a literal
then if y is a literal
then literal sum
else if y is an opp
then x - y
else x + y
else if y is an opp
then x - y
else if x is an opp
then y - x
else x + y
where we actually want the code
fun x y
=> if x is a literal
then if y is a literal
then return (literal sum);
if y is an opp
then return (x - y);
if x is an opp
then return (y - x);
return (x + y)
in the sequence+return monad. i.e., we want to not duplicate the "if y
is an opp" code multiple times.
I think the solution to this is to have the discrimination tree
evaluator return an option, and to have the function that computes the
discrimination tree not duplicate rewrite rules among different cases.
Note that this leads to slightly inefficient matching sometimes: when
two rules with the same structure are separated by a rule with a
wildcard instead of structure, we will now try to match on the structure
twice. It might be useful to be able to denote that some rewrite rules
can be commuted.
After | File Name | Before || Change | % Change
----------------------------------------------------------------------------------------------------------------------
40m35.83s | Total | 30m00.99s || +10m34.84s | +35.24%
----------------------------------------------------------------------------------------------------------------------
21m46.37s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 6m01.39s || +15m44.97s | +261.48%
6m37.40s | p384_32.c | 0m22.47s || +6m14.92s | +1668.58%
0m18.00s | Experiments/NewPipeline/Rewriter | 5m16.50s || -4m58.50s | -94.31%
0m30.49s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 1m54.20s || -1m23.71s | -73.30%
0m27.41s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 1m39.40s || -1m11.99s | -72.42%
0m47.78s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 1m54.50s || -1m06.71s | -58.27%
0m40.28s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 1m23.77s || -0m43.48s | -51.91%
0m15.21s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m55.86s || -0m40.64s | -72.77%
0m23.39s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 1m00.22s || -0m36.82s | -61.15%
0m21.85s | p256_32.c | 0m04.01s || +0m17.84s | +444.88%
0m20.97s | secp256k1_32.c | 0m03.26s || +0m17.71s | +543.25%
0m04.60s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m20.33s || -0m15.72s | -77.37%
0m09.48s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m23.28s || -0m13.80s | -59.27%
1m33.63s | Experiments/NewPipeline/Toplevel2 | 1m45.56s || -0m11.93s | -11.30%
0m08.29s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m18.64s || -0m10.35s | -55.52%
0m05.93s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m16.74s || -0m10.80s | -64.57%
0m32.41s | p521_64.c | 0m41.42s || -0m09.01s | -21.75%
0m04.93s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m14.92s || -0m09.99s | -66.95%
0m04.40s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m12.57s || -0m08.16s | -64.99%
0m08.52s | p224_32.c | 0m01.95s || +0m06.56s | +336.92%
0m13.99s | p384_64.c | 0m10.64s || +0m03.34s | +31.48%
4m07.13s | Experiments/NewPipeline/Toplevel1 | 4m05.83s || +0m01.29s | +0.52%
0m38.96s | p521_32.c | 0m40.09s || -0m01.13s | -2.81%
0m02.28s | p224_64.c | 0m01.66s || +0m00.61s | +37.34%
0m02.27s | curve25519_32.c | 0m01.98s || +0m00.29s | +14.64%
0m01.78s | p256_64.c | 0m01.65s || +0m00.13s | +7.87%
0m01.70s | secp256k1_64.c | 0m01.96s || -0m00.26s | -13.26%
0m01.65s | curve25519_64.c | 0m01.51s || +0m00.13s | +9.27%
0m01.37s | Experiments/NewPipeline/CLI | 0m01.26s || +0m00.11s | +8.73%
0m01.15s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.21s || -0m00.06s | -4.95%
0m01.14s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.16s || -0m00.02s | -1.72%
0m01.07s | Experiments/NewPipeline/CompilersTestCases | 0m01.05s || +0m00.02s | +1.90%
|
Jason Gross
Jason Gross