Stream: git-wasmtime

Topic: wasmtime / issue #5705 ISLE: make `subsume` a built-in

Wasmtime GitHub notifications bot (Feb 03 2023 at 22:24):

jameysharp opened issue #5705:

Feature

Our mid-end optimization rules define a special constructor called subsume in prelude_opt.isle. Its effect is to cause the e-graph optimization pass to ignore other results from the same call to simplify. Let's consider making it a feature of the ISLE language instead, applicable to any multi-term.

Background

For a rule-driven multi-constructor term, ISLE currently generates a Rust function which accumulates results into a Vec. It returns the whole vector once all pattern matches have completed.

The e-graph specific implementation of subsume records all values it's called on in the optimization context. After all pattern matches have finished, optimize_pure_enode checks each value from the accumulated vector to see if it is one where subsume was used. The first one it finds causes the rest of the vector to be skipped, and returns a singleton e-class. However any earlier values were already added to the e-graph; they're effectively hidden from elaboration but still taking memory.

This is used for any rule where we know ahead of time that if the rule matches, it will produce a result which is at least as good as any other rule we might pick. It's primarily used for rules which rewrite an expression into a constant.

Benefit

If ISLE were aware of the semantics of subsume, it could apply two optimizations to the generated code:

• The first rule which matches and is flagged as subsume could return early with a singleton vector. Then the caller doesn't have to process any results that it's going to ignore, and the simplify function doesn't have to evaluate later pattern matches whose results will be ignored anyway.

• Rules flagged subsume could be checked before other rules, if that allows us to check fewer patterns. This isn't trivial to get right but could be a nice compile-time win.

Making subsume a part of the language is also useful for static analysis purposes, like #5704, or checking if such rules fully shadow other rules.

This would allow subsume-like behavior in multi-terms other than simplify. I don't have a use-case in mind for that but it might be useful for something. Currently I think any multi-term could call subsume and maybe do something useful with it, but it would be difficult to use correctly anywhere except at the top-level of the right-hand side of rules in simplify.

Implementation

I'm imagining an optional keyword after (rule but before the left-hand side.

Alternatives

We could define rule priorities in multi-terms to mean that all rules of the same priority have their results returned together, and only the highest priority which matches any rule is returned. That might be a useful generalization of "subsumes", or it might just make the rules harder to reason about.

Wasmtime GitHub notifications bot (Feb 04 2023 at 00:05):

cfallin commented on issue #5705:

This is really interesting to me because it diverges significantly from my mental model / layering -- worth digging into why, I think!

subsume was at least originally meant to be an egraph-specific intrinsic, and I think this can still be seen today in behavior that islec could not replicate purely by itself if subsume were just a way to alter multi-term behavior: the subsuming value replaces even the original input to the rewrite in the value-map as we build the egraph. In other words, if we subsume an expression with a constant due to cprop, it's not just that we return only that iconst Value and nothing else; it's that the toplevel loop that would ordinarily build an eclass out of the input (rewritten) value and its various rewrites, instead takes just the one rewrite.

Seen another way, this would mean that the conceptual Iterator<Item = Value> return from the simplify multi-term would instead need to turn into something like Iterator<Item = MaybeSubsumingValue> where enum MaybeSubsumingValue { Normal(Value), Subsuming(Value) }. We could do something like that but...

What I do like instead is that islec has special knowledge of a property of the subsume constructor, such that it tries to evaluate these rules first, as you suggest. I think it should be on subsume, and not on rules that use it (else we're liable to forget it); and should perhaps be something like (decl shortcut subsume (Value) Value) where shortcut means "the RHS evaluating this ctor can return its value alone". We still need the external ctor call to actually make the above behavior happen though.

All of that said, while writing the last paragraph, the sum-type approach is actually starting to grow on me. Perhaps what we want is a subsume, marked with shortcut, that builds a (MaybeSubsumingValue.Subsuming x) from x; and an implicit converter otherwise that builds a (MaybeSubsumingValue.Normal x) from x. Thoughts?

Wasmtime GitHub notifications bot (Feb 14 2023 at 19:48):

jameysharp commented on issue #5705:

We discussed subsume yesterday and concluded that we should try treating it as an egraph-specific dynamic property of the result of simplify, rather than something we annotate on individual rules. There could still be an advantage to having some way to make simplify return early, but until we have a clearer idea of exactly which shortcuts we want I don't think we should put too much thought into that aspect. So I'm retracting this idea, at least for now.

Wasmtime GitHub notifications bot (Feb 14 2023 at 19:48):

jameysharp closed issue #5705:

Feature

Our mid-end optimization rules define a special constructor called subsume in prelude_opt.isle. Its effect is to cause the e-graph optimization pass to ignore other results from the same call to simplify. Let's consider making it a feature of the ISLE language instead, applicable to any multi-term.

Background

For a rule-driven multi-constructor term, ISLE currently generates a Rust function which accumulates results into a Vec. It returns the whole vector once all pattern matches have completed.

The e-graph specific implementation of subsume records all values it's called on in the optimization context. After all pattern matches have finished, optimize_pure_enode checks each value from the accumulated vector to see if it is one where subsume was used. The first one it finds causes the rest of the vector to be skipped, and returns a singleton e-class. However any earlier values were already added to the e-graph; they're effectively hidden from elaboration but still taking memory.

This is used for any rule where we know ahead of time that if the rule matches, it will produce a result which is at least as good as any other rule we might pick. It's primarily used for rules which rewrite an expression into a constant.

Benefit

If ISLE were aware of the semantics of subsume, it could apply two optimizations to the generated code:

• The first rule which matches and is flagged as subsume could return early with a singleton vector. Then the caller doesn't have to process any results that it's going to ignore, and the simplify function doesn't have to evaluate later pattern matches whose results will be ignored anyway.

• Rules flagged subsume could be checked before other rules, if that allows us to check fewer patterns. This isn't trivial to get right but could be a nice compile-time win.

Making subsume a part of the language is also useful for static analysis purposes, like #5704, or checking if such rules fully shadow other rules.

This would allow subsume-like behavior in multi-terms other than simplify. I don't have a use-case in mind for that but it might be useful for something. Currently I think any multi-term could call subsume and maybe do something useful with it, but it would be difficult to use correctly anywhere except at the top-level of the right-hand side of rules in simplify.

Implementation

I'm imagining an optional keyword after (rule but before the left-hand side.

Alternatives

We could define rule priorities in multi-terms to mean that all rules of the same priority have their results returned together, and only the highest priority which matches any rule is returned. That might be a useful generalization of "subsumes", or it might just make the rules harder to reason about.

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

jameysharp commented on issue #5705:

We're tracking the new plan for subsume in #6105.

Last updated: Dec 23 2024 at 12:05 UTC