Stream: git-wasmtime

Topic: wasmtime / issue #4129 Cranelift: develop a generic lazy ...

Wasmtime GitHub notifications bot (May 10 2022 at 23:24):

cfallin opened issue #4129:

As part of #4128, we should develop a lazy analysis framework that permits us to easily compute properties of CLIF values, operators, or program points between operators (depending on the analysis). This framework should accept pluggable lattice types, lattice meet functions, and transfer functions, ideally permitting these to be written in ISLE.

We should look into the following ideas:

• Perhaps it is possible to avoid an iterative dataflow-analysis fixpoint by not supporting cyclic analysis at all. Many analyses can't say something meaningful about cycles anyway, at least when the cycle exists due to a non-redundant blockparam (i.e., actually multiple reaching definitions). If we stop at cycles (and immediately shortcut to the lattice "bottom" value), we can lazily go up the DAG of operators, memoizing analysis results per Value as we come back down.

  • Note that supporting fixpoint analysis of forward-dataflow properties is difficult with CLIF in any case because we don't have use-lists per Value, so we can't propagate forward unless we build that information on the side.

• Perhaps it is possible to co-mingle the analysis with mutations performed by a mid-end optimization framework by either reasoning about invalidations, or else constraining rewrites in a pass of the appropriate direction (e.g., an analysis that "looks upward" and stops at cycles is always safe to lazily complete while doing a downward pass, as long as one sees defs before uses).

Wasmtime GitHub notifications bot (May 10 2022 at 23:24):

cfallin labeled issue #4129:

As part of #4128, we should develop a lazy analysis framework that permits us to easily compute properties of CLIF values, operators, or program points between operators (depending on the analysis). This framework should accept pluggable lattice types, lattice meet functions, and transfer functions, ideally permitting these to be written in ISLE.

We should look into the following ideas:

• Perhaps it is possible to avoid an iterative dataflow-analysis fixpoint by not supporting cyclic analysis at all. Many analyses can't say something meaningful about cycles anyway, at least when the cycle exists due to a non-redundant blockparam (i.e., actually multiple reaching definitions). If we stop at cycles (and immediately shortcut to the lattice "bottom" value), we can lazily go up the DAG of operators, memoizing analysis results per Value as we come back down.

  • Note that supporting fixpoint analysis of forward-dataflow properties is difficult with CLIF in any case because we don't have use-lists per Value, so we can't propagate forward unless we build that information on the side.

• Perhaps it is possible to co-mingle the analysis with mutations performed by a mid-end optimization framework by either reasoning about invalidations, or else constraining rewrites in a pass of the appropriate direction (e.g., an analysis that "looks upward" and stops at cycles is always safe to lazily complete while doing a downward pass, as long as one sees defs before uses).

Wasmtime GitHub notifications bot (May 10 2022 at 23:24):

cfallin labeled issue #4129:

As part of #4128, we should develop a lazy analysis framework that permits us to easily compute properties of CLIF values, operators, or program points between operators (depending on the analysis). This framework should accept pluggable lattice types, lattice meet functions, and transfer functions, ideally permitting these to be written in ISLE.

We should look into the following ideas:

• Perhaps it is possible to avoid an iterative dataflow-analysis fixpoint by not supporting cyclic analysis at all. Many analyses can't say something meaningful about cycles anyway, at least when the cycle exists due to a non-redundant blockparam (i.e., actually multiple reaching definitions). If we stop at cycles (and immediately shortcut to the lattice "bottom" value), we can lazily go up the DAG of operators, memoizing analysis results per Value as we come back down.

  • Note that supporting fixpoint analysis of forward-dataflow properties is difficult with CLIF in any case because we don't have use-lists per Value, so we can't propagate forward unless we build that information on the side.

• Perhaps it is possible to co-mingle the analysis with mutations performed by a mid-end optimization framework by either reasoning about invalidations, or else constraining rewrites in a pass of the appropriate direction (e.g., an analysis that "looks upward" and stops at cycles is always safe to lazily complete while doing a downward pass, as long as one sees defs before uses).

Wasmtime GitHub notifications bot (May 11 2022 at 17:14):

fitzgen commented on issue #4129:

• Note that supporting fixpoint analysis of forward-dataflow properties is difficult with CLIF in any case because we don't have use-lists per Value, so we can't propagate forward unless we build that information on the side.

We can do the more abstract interpretation-y implementation of the forwards analysis (rather than the work queue-y implementation that would rely on use lists) by walking blocks and walking each instruction in a block and doing the analysis for each instruction that way, no?

Wasmtime GitHub notifications bot (May 11 2022 at 17:41):

cfallin commented on issue #4129:

Yes, but it runs into the same problem with cycles whether we do it lazily (reaching backward on request) or eagerly (walking forward and evaluating for each new def): when we hit a blockparam, what do we do? Walking backward, we might recurse over the edge and find a cycle; we need a way to take some initial value, but remember to "come back" later (hence side-info). Walking forward, we have to plug in some initial value but again we need to record the loop and come back to it.

In other words I think that the supporting-cycles-with-fixpoint feature and the lazy-backward-or-eager-forward decision are orthogonal; the former requires additional info (esssentially, for us to reify the graph somehow so we can iterate over it) whether or not we do the latter.

Wasmtime GitHub notifications bot (May 18 2022 at 05:30):

cfallin commented on issue #4129:

I've done some initial prototyping work in this direction over the past week or so in this branch (somewhat misnamed isle-memoization as it's really an eager approach now):

• Initially I tried to work out the scheme described here in more complete detail. I had wanted to build a fully lazy scheme to allow for "sparse facts": analyses that only need to look at a subset of values, rather than eagerly fill a table for every value, program point, or instruction.
• The main difficulty I ran into was in avoiding unbounded (input-controlled) recursion while not completely rewriting the ISLE compiler. The straightforward way do to lazy memoized evaluation in ISLE is to add a bit to the start of a generated function body that checks a table and returns if memoized, and a bit at each return point to record the result. But if we recurse "up the function body" to compute a property down a dataflow chain, (i) this is not tail recursion, because we have to store the tuples on the way back down, and so (ii) we have unbounded stack growth, and the fuzzers will eat this for breakfast (i.e.: we can't do that).
• One could in principle solve that by compiling to a form with an explicit stack instead. Basically, turn the ISLE code into a state machine with a stack. (Sound familiar @fitzgen? :-) ) But (i) I don't really think it's prudent to rewrite the ISLE compiler at this stage for dubious benefits and (ii) indeed I think there would be dubious benefits: the performance characteristics of an explicit "interpreter loop over FSM states" are much different than the 1-to-1 compilation strategy to Rust that we have today.

So then I began to work out an eager approach (roughly, Datalog-like rather than Prolog-like, for anyone familiar with both): scan the function top to bottom and evaluate an ISLE constructor at each {value, instruction, program point} (depending on analysis), filling a table in. That's what the branch linked above is.

The two major issues with this are:

• There are relations/properties that really do want to be sparse. In developing alias analysis and redundant-loads (see branch), one ideally wants to build a map from (memory alias state, address SSA value, type) keys to known-value-stored-at-that-address values. We definitely do not want to scan that whole key-space eagerly.
• There are possibly some ways around this by playing with the key and value definitions, but I started to realize I wanted tuple types in ISLE, and that is a whole other rabbithole I'd prefer to avoid...
• And in general, I realized the following basic reality: ISLE is (so far, in today's state) not a general-enough language for analysis, together with: the kinds of optimizations we want to do in analyses to be efficient are a bit too general-purpose for a rigid term-rewriting worldview.

Said another way, I was pushing the design above in the direction of Prolog/Datalog because I know that these can be used for general and powerful program analysis (I've done it!) but there are additional tricks one does there that ISLE can't express.

In addition to that, on a more subjective level, I was starting to approach and slightly exceed my complexity-budget comfort level in that branch ("is this really better than hand-coding X...?").

So I think I want to conclude now, given the few weeks' experimentation here, that the analyses should not (yet) be in ISLE, though the mid-end rewrites can probably still be, as the language is explicitly a pattern-rewriting language now. In the fullness of time, we might be able to revisit this, and get the benefits (chiefly: fusing with lowering, and ability to formally verify analyses); but let's not force it before its time.

(I'll leave this issue open as an "enhancement" in the tracker to keep these ideas around for that future time!)

Wasmtime GitHub notifications bot (Nov 02 2022 at 16:22):

fitzgen commented on issue #4129:

I think we can close this? We have a (Rust, not ISLE) framework with the recent e-graphs stuff.

Wasmtime GitHub notifications bot (Nov 02 2022 at 17:05):

cfallin commented on issue #4129:

Yes, I think so; we've found that the best balance of design concerns here lands at in-Rust analyses, but we have a general forward-direction analysis framework now, so I'll close this.

Wasmtime GitHub notifications bot (Nov 02 2022 at 17:05):

cfallin closed issue #4129:

As part of #4128, we should develop a lazy analysis framework that permits us to easily compute properties of CLIF values, operators, or program points between operators (depending on the analysis). This framework should accept pluggable lattice types, lattice meet functions, and transfer functions, ideally permitting these to be written in ISLE.

We should look into the following ideas:

• Perhaps it is possible to avoid an iterative dataflow-analysis fixpoint by not supporting cyclic analysis at all. Many analyses can't say something meaningful about cycles anyway, at least when the cycle exists due to a non-redundant blockparam (i.e., actually multiple reaching definitions). If we stop at cycles (and immediately shortcut to the lattice "bottom" value), we can lazily go up the DAG of operators, memoizing analysis results per Value as we come back down.

  • Note that supporting fixpoint analysis of forward-dataflow properties is difficult with CLIF in any case because we don't have use-lists per Value, so we can't propagate forward unless we build that information on the side.

• Perhaps it is possible to co-mingle the analysis with mutations performed by a mid-end optimization framework by either reasoning about invalidations, or else constraining rewrites in a pass of the appropriate direction (e.g., an analysis that "looks upward" and stops at cycles is always safe to lazily complete while doing a downward pass, as long as one sees defs before uses).

Last updated: Nov 22 2024 at 16:03 UTC