Stream: git-wasmtime

Topic: wasmtime / issue #5704 ISLE/egraphs: static analysis for ...

Wasmtime GitHub notifications bot (Feb 03 2023 at 21:01):

jameysharp opened issue #5704:

Feature

It's not obvious to me when to use subsume in mid-end optimization rules. At the least we should document what principles a rule author should follow to decide whether to use this feature or not. But I think there's a chance that these principles will turn out to be mechanizable, or at least some conservative approximation of them. Ideally we'd be able to check this in the ISLE compiler like we do with overlap checks, but a separate verifier that we can run in CI would be okay too.

Benefit

The subsume operation is an important compile-time optimization in our egraph framework, because it allows us to prune egraph nodes that we're confident aren't any better than the subsumed expression. That saves memory as well as reducing the runtime of later pattern-matches and of elaboration.

However, if we overuse subsume we can miss optimization opportunities. If we can prove that subsume is only used in cases which are at least as good as all alternatives, by some measure, then we can be confident that we're getting the best optimization results we can from our rule set.

Implementation

One idea is to check any pair of rules which overlap, where at least one uses subsume.

• If we can prove that both rules produce the same result on all inputs where the two rules both match, then subsume is safe because it doesn't matter which rule we pick. This is easiest for rules which reduce to one of their input bindings, or use an identical tree of constructors; we can check that both rules reduce to the same binding site.
• If only one of the pair uses subsume, and we can prove that its result is never worse than the other rule when both rules match, then subsume is a good choice. This requires picking a cost model.

Proving equivalence in general might require SMT solving, for rules whose left-hand sides use constructors like u64_sub. But maybe a conservative approximation will allow enough rules that we can express what we need to without requiring full equivalence proofs.

Alternatives

At minimum, we should document some guidance for rule authors.

Wasmtime GitHub notifications bot (Feb 04 2023 at 02:06):

jameysharp commented on issue #5704:

Another alternative that comes to mind is to remove subsume entirely. The more I look at the existing rules, I think subsume is appropriate if, and only if, a rule evaluates to a constant. That's a property we could check dynamically in the egraph code without needing any annotation in ISLE rules.

Treating constants specially might be a good idea for other reasons too. We might get a compile-time performance boost by keeping a separate map from Value to constant. Any rules which need to match on a constant value could look it up in O(1) time from the map, instead of needing to iterate through the entire e-class to find out whether there are any iconst instructions in it.

I guess the other case where subsume might be reasonable is when the rule rewrites to an existing instruction, rather than constructing a new one. That's also a property we can identify dynamically instead of annotating it. It's not clear to me that it's always a good idea though.

Wasmtime GitHub notifications bot (Feb 04 2023 at 03:04):

cfallin commented on issue #5704:

I think there could be some simple rules here, indeed.

I want to inject a little caution around simplicity, in the sense that if we end up having to reason about a rule with subsume interacting with other rules, or proving any results from that, we're maybe on the wrong path. (I can't quite articulate why, but that gives me a deep sense of unease and makes me want to pull the complexity handbrake. It's too much effort for too little payoff, and too much complexity to maintain and carry forward. Overlap is a fundamental property and one that matters for correctness, while subsumption is an efficiency thing, and islec maybe shouldn't be in the business of trying to understand how rule outputs interact with other rule inputs or what nodes' costs are, at least not yet.)

I think your two cases are onto something though -- the "resolves to constant" and "resolves to sub-part of original expression" are the two cases where I've used subsume, and I think those are probably reasonable to stick to for now. We could maybe build a separate pass, as you say, that recognizes legal inputs to subsume. Possibly via annotations with custom tags: subsume requires subsume_valid on its input, iconst produces a value with subsume_valid, and all variable captures from the LHS are automatically tagged subsume_valid. (Insert bikeshedding here about how to annotate that.) Or we annotate both subsume and iconst as "lang items" that islec's pass can reason about directly.

As long as this remains a predicate that can reason about an RHS expression subtree within one rule, without any context from other rules, I'm happy!

Wasmtime GitHub notifications bot (Feb 06 2023 at 17:13):

jameysharp commented on issue #5704:

Yeah, the problem that motivated me to open this issue is that I can't reason about the use of subsume today. It's a claim that no other rule would produce a result that is "better" than this one. That is fundamentally an interaction between all rules. So I think we're already in the situation you're worried about.

It's probably okay for constants: since Cranelift doesn't have undefined values, if some valid simplification of an expression yields a constant, then all ways of evaluating that expression must yield the same constant.

It isn't actually obvious to me that it's okay for "resolves to sub-part of original expression". For some rule that simplifies to a sub-part, I think there could be another rule which is identical except for also matching deeper into the sub-part, and the latter rule could produce a "better" result because it's examining more of the input.

Wasmtime GitHub notifications bot (Feb 14 2023 at 20:33):

jameysharp commented on issue #5704:

We discussed this yesterday. The only situation where we're confident that subsume is sensible is the "resolves to constant" case. For that specific case, we don't need to annotate any rules; we can dynamically check the values that simplify returns to see if any of them are constants, and trigger the current subsume behavior accordingly.

Wasmtime GitHub notifications bot (Mar 27 2023 at 19:34):

jameysharp commented on issue #5704:

We're going to remove subsume instead: #6105

Wasmtime GitHub notifications bot (Mar 27 2023 at 19:34):

jameysharp closed issue #5704:

Feature

It's not obvious to me when to use subsume in mid-end optimization rules. At the least we should document what principles a rule author should follow to decide whether to use this feature or not. But I think there's a chance that these principles will turn out to be mechanizable, or at least some conservative approximation of them. Ideally we'd be able to check this in the ISLE compiler like we do with overlap checks, but a separate verifier that we can run in CI would be okay too.

Benefit

The subsume operation is an important compile-time optimization in our egraph framework, because it allows us to prune egraph nodes that we're confident aren't any better than the subsumed expression. That saves memory as well as reducing the runtime of later pattern-matches and of elaboration.

However, if we overuse subsume we can miss optimization opportunities. If we can prove that subsume is only used in cases which are at least as good as all alternatives, by some measure, then we can be confident that we're getting the best optimization results we can from our rule set.

Implementation

One idea is to check any pair of rules which overlap, where at least one uses subsume.

• If we can prove that both rules produce the same result on all inputs where the two rules both match, then subsume is safe because it doesn't matter which rule we pick. This is easiest for rules which reduce to one of their input bindings, or use an identical tree of constructors; we can check that both rules reduce to the same binding site.
• If only one of the pair uses subsume, and we can prove that its result is never worse than the other rule when both rules match, then subsume is a good choice. This requires picking a cost model.

Proving equivalence in general might require SMT solving, for rules whose left-hand sides use constructors like u64_sub. But maybe a conservative approximation will allow enough rules that we can express what we need to without requiring full equivalence proofs.

Alternatives

At minimum, we should document some guidance for rule authors.

Last updated: Oct 23 2024 at 20:03 UTC