-
Notifications
You must be signed in to change notification settings - Fork 1.6k
Cranelift: Use a fixpoint loop to compute the best value for each eclass #7859
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
7 commits
Select commit
Hold shift + click to select a range
a353b5d
Cranelift: Use a fixpoint loop to compute the best value for each eclass
fitzgen 370fb43
Remove fixpoint loop early-continue optimization
fitzgen b5c3d4b
Add document describing optimization rule invariants
fitzgen 04c2d53
Make select optimizations use subsume
fitzgen 9c1d078
Remove invalid debug assert
fitzgen e164dcf
Remove now-unused methods
fitzgen e04c4d4
Add commutative adds to cost tests
fitzgen File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or 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
This file contains hidden or 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
This file contains hidden or 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
This file contains hidden or 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,5 +1,81 @@ | ||
| Rules here are allowed to rewrite pure expressions arbitrarily, | ||
| using the same inputs as the original, or fewer. In other words, we | ||
| cannot pull a new eclass id out of thin air and refer to it, other | ||
| than a piece of the input or a new node that we construct; but we | ||
| can freely rewrite e.g. `x+y-y` to `x`. | ||
| # Rules for Writing Optimization Rules | ||
|
|
||
| For both correctness and compile speed, we must be careful with our rules. A lot | ||
| of it boils down to the fact that, unlike traditional e-graphs, our rules are | ||
| *directional*. | ||
|
|
||
| 1. Rules should not rewrite to worse code: the right-hand side should be at | ||
| least as good as the left-hand side or better. | ||
|
|
||
| For example, the rule | ||
|
|
||
| x => (add x 0) | ||
|
|
||
| is disallowed, but swapping its left- and right-hand sides produces a rule | ||
| that is allowed. | ||
|
|
||
| Any kind of canonicalizing rule that intends to help subsequent rules match | ||
| and unlock further optimizations (e.g. floating constants to the right side | ||
| for our constant-propagation rules to match) must produce canonicalized | ||
| output that is no worse than its noncanonical input. | ||
|
|
||
| We assume this invariant as a heuristic to break ties between two | ||
| otherwise-equal-cost expressions in various places, making up for some | ||
| limitations of our explicit cost function. | ||
|
|
||
| 2. Any rule that removes value-uses in its right-hand side that previously | ||
| existed in its left-hand side MUST use `subsume`. | ||
|
|
||
| For example, the rule | ||
|
|
||
| (select 1 x y) => x | ||
|
|
||
| MUST use `subsume`. | ||
|
|
||
| This is required for correctness because, once a value-use is removed, some | ||
| e-nodes in the e-class are more equal than others. There might be uses of `x` | ||
| in a scope where `y` is not available, and so emitting `(select 1 x y)` in | ||
| place of `x` in such cases would introduce uses of `y` where it is not | ||
| defined. | ||
|
|
||
| 3. Avoid overly general rewrites like commutativity and associativity. Instead, | ||
| prefer targeted instances of the rewrite (for example, canonicalizing adds | ||
| where one operand is a constant such that the constant is always the add's | ||
| second operand, rather than general commutativity for adds) or even writing | ||
| the "same" optimization rule multiple times. | ||
|
|
||
| For example, the commutativity in the first rule in the following snippet is | ||
| bad because it will match even when the first operand is not an add: | ||
|
|
||
| ;; Commute to allow `(foo (add ...) x)`, when we see it, to match. | ||
| (foo x y) => (foo y x) | ||
|
|
||
| ;; Optimize. | ||
| (foo x (add ...)) => (bar x) | ||
|
|
||
| Better is to commute only when we know that canonicalizing in this way will | ||
| all definitely allow the subsequent optimization rule to match: | ||
|
|
||
| ;; Canonicalize all adds to `foo`'s second operand. | ||
| (foo (add ...) x) => (foo x (add ...)) | ||
|
|
||
| ;; Optimize. | ||
| (foo x (add ...)) => (bar x) | ||
|
|
||
| But even better in this case is to write the "same" optimization multiple | ||
| times: | ||
|
|
||
| (foo (add ...) x) => (bar x) | ||
| (foo x (add ...)) => (bar x) | ||
|
|
||
| The cost of rule-matching is amortized by the ISLE compiler, where as the | ||
| intermediate result of each rewrite allocates new e-nodes and requires | ||
| storage in the dataflow graph. Therefore, additional rules are cheaper than | ||
| additional e-nodes. | ||
|
|
||
| Commutativity and associativity in particular can cause huge amounts of | ||
| e-graph bloat. | ||
|
|
||
| One day we intend to extend ISLE with built-in support for commutativity, so | ||
| we don't need to author the redundant commutations ourselves: | ||
| https://github.com/bytecodealliance/wasmtime/issues/6128 |
Oops, something went wrong.
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.
Uh oh!
There was an error while loading. Please reload this page.