Proposal Details
Technically, this is an internal change and I don't think it requires a proposal, but it is pretty substantial and people have already offered valuable feedback, so sending it to a wider audience:
eSSA for go's prove pass
Go's prove pass has served us well over the years, but the dominator-based algorithm has some drawbacks:
-
constraints that are true over all incoming paths, but are not established in a dominator, get missed. The prototypical example of this is min/max, which we currently handle specially
but small variations in code construction can evade our pattern matching. For example, an equivalent min/max construction over a pointer:
x := f.field
if x == nil {
x = new(int)
}
The subsequent uses of x will not have any nil checks pruned (by the prove pass at least, we still catch this in late nilcheckelim)
-
Induction variables are handled specially. With SIMD variants of loops on the horizon, the constructions that we use for loop variables are liable to change and defeat our pattern matching.
We already have one special case solution for this in the form of the chunked iteration pattern matcher, but a more general solution would be preferable.
-
Values having multiple ranges at different times during the analysis makes either replacing them or tagging them with information for a subset of blocks difficult. The simplifyBlock step
handles some of these, but the replacements are written ad-hoc. Leveraging our opt pattern matching infrastructure could help us catch more cases. A recent example of this problem
is https://go.dev/cl/785801
For these reasons, I propose that we replace the dominator-based algorithm with a two-stage dataflow range analysis and bounds-check elimination procedure, centered around eSSA.
Extended SSA
Extended SSA (eSSA) is a form of SSA where uses in conditionals that denote a range or ordering get turned into new copies of said value. These copies can then serve as stand-ins for "Value x at execution point y". For us, this enables two things that help with running range analysis dataflow quickly:
- The dataflow equations become control-flow independent without giving up precision. For a given value, we can update it's information in place while solving and we no longer have to worry about either maintaining range or ordering stacks.
- eSSA enables sparse solutions to dataflow propagation. If a condition is added, or a new range is discovered for a given value via a control, then only the uses that directly depend on this new information will have to be reevaluated.
The tradeoff is that this form needs to be constructed before we can run our analysis. The current prototype I have does this with linear time algorithms only and takes 24.8 microseconds on a function that takes 69.0 microseconds to run the entire prove pass on.
A bonus of these new copies: they have their own storage. Marking them, either via Aux or an array in Func, would allow for later pattern matching in a .rules file
An example of a min function in eSSA form. Conventionally, the copies are sigma or pi operations. Here, we use single-arity phi nodes.
Before eSSA conversion:
min func(int, int) int
b1:
(?) v1 = InitMem <mem>
(-3) v7 = Arg <int> {a} (a[int], y[int])
(-3) v8 = Arg <int> {b} (b[int], y[int])
(+5) v10 = Less64 <bool> v7 v8
If v10 -> b3 b4
b2: <- b3 b4
(10) v13 = Phi <int> v7 v8 (y[int])
(+10) v15 = MakeResult <int,mem> v13 v1
Ret v15
b3: <- b1
Plain -> b2
b4: <- b1
Plain -> b2
After eSSA conversion:
min func(int, int) int
b1:
(?) v1 = InitMem <mem>
(-3) v7 = Arg <int> {a} (a[int], y[int])
(-3) v8 = Arg <int> {b} (b[int], y[int])
(+5) v10 = Less64 <bool> v7 v8
If v10 -> b3 b4
b2: <- b3 b4
(10) v13 = Phi <int> v12 v9 (y[int])
(+10) v15 = MakeResult <int,mem> v13 v1
Ret v15
b3: <- b1
(-3) v12 = Phi <int> v7 <-------------------- NEW
Plain -> b2
b4: <- b1
(-3) v9 = Phi <int> v8 <--------------------- NEW
Plain -> b2
These values will then be incorporated into the dataflow, denoting that v12 is less than v8 (because the positive branch was taken) and v9 is less than or equal v7 (because the negative branch was taken). Phis with multiple predecessors combine these orderings and the range information they denote. v13 in the above example will be less than v8 and less than or equal v7.
Instead of using the poset data structure for checking whether constraints are consistent after a branch, we can now perform the depth-first search directly on the use-def chain, since it now encodes orderings. This avoids having to build the posets DAG and removes the need for checkpointing and restoring.
Range analysis
For range analysis, I propose that we use a dataflow solution to propagate range information. Usually, this requires as many dataflow passes over the CFG as the height of your lattice, and for range analysis, this would be infinite. We avoid some of this expense by employing 2 techniques.
- Aggressive widening/narrowing.
- Bias towards strongly connected components during solve.
Widening/narrowing
While doing our dataflow analysis, we might find the need to revisit a value. Consider the following code:
s := 0
for i := 0; i < 200; i++ {
s += i
}
return s
Which turns into the following eSSA code:
b1:
(?) v7 = Const64 <int> [0] (i[int], s[int])
(?) v9 = Const64 <int> [200]
(?) v15 = Const64 <int> [1]
Plain -> b2
b2: <- b1 b4
(15) v8 = Phi <int> v7 v16 (i[int])
(15) v21 = Phi <int> v7 v13 (s[int])
(+15) v10 = Less64 <bool> v8 v9
If v10 -> b4 b5 (likely)
b4: <- b2
(-15) v18 = Phi <int> v8
(+16) v13 = Add64 <int> v21 v18 (s[int])
(+15) v16 = Add64 <int> v15 v18 (i[int])
Plain -> b2
b5: <- b2
(+18) v19 = MakeResult <int,mem> v21 v1
Ret v19
Here, we will focus on v8 and v18, two versions of our induction variable. During the initial stage of our solution, we will find v8 to have [0,0] as a range (because v16 is yet to be visited). This value will flow through v18 [0,0], v16 [1,1] and then finally back to v8. If we naively update our range to the union of v7 and v16 [0,1], we will find ourself revisiting this loop until our Less64 conditional restrains our range, visiting this loop 200 times.
To solve this problem, we employ widening. Whenever we revisit a value, we'll inspect in which ways the bounds of our range grow. For our worked example, the second visit of v8 indicates a growing upper bound. With the initial state, the range will then come out to [0,inf]. This will flow through the conditional at v10 and be narrowed to [0,199].
In practice, this means that we will visit values twice. Once to initialize the base case or discover the growth of a variable, and once to propagate the widened value.
Note that s (v21) in our example gets a similar treatment to i, progressing through v21[0,0], v13[1,1], v21[0,inf] (because of widening), v13[-inf,inf] (because of overflow) and then finally v21[-inf,inf]. Calculating the final value of s is possible with a scalar evolution pass, but outside the scope of this proposal.
Bias towards strongly connected components during solve
Solving dataflow systems relies on iterating over the CFG until a fixed point is reached. This can involve multiple passes over a CFG, where state is evaluated, just to find that no update needs to be done.
To reduce the runtime of the analysis, we will instead solve by strongly connected component (SCC). By iterating over an SCC until it reaches a fixed point, we avoid having to revisit any of the values later on in the solve. This also interacts advantageously with widening. A value that is found to be widened in both lower bound and upper bound may in actuality only grow in one bound. Whether we discover this is dependent on the order in which we visit values. Doing the analysis by SCC will give more conservative ranges to be propagated to other values.
SCCs in Go are roughly analogous to loops. Here we can use the loop nesting forest to guide our solve. When enqueuing a value for analysis, we use a priority queue indexed on the loop depth of its block. By processing outer loops first, we ensure that the initial conditions for inner loops are established before we try to solve them. Occasionally, an inner loop may expose a value to an outer loop, but because we've run growth analysis on the outer loop already, it is unlikely to change the established range of any values.
Note that our current loop nesting forest only handles reducible CFGs and when an irreducible CFG is found, the loop to SCC equivalence is broken. These irreducible CFGs can only be constructed using gotos and are exceedingly rare. For example, there is only one instance of such a CFG in the standard library, and it is in a non performance-sensitive spot. For the initial implementation, I intend to ignore SCCs in functions with irreducible control flow, but future work may include changing our loop nesting forest definition, or running a pass before prove which would make the control flow reducible.
Constraint system
Range analysis by itself is fairly limited about what it can do as far as eliminating bounds checks. Since the length of a slice is initially unknown and come from outside context (for example, a slice being passed as a parameter to a function), numerical methods can only do so much. The vast majority of bounds checks that are eliminated currently happen by finding a check unsatisfiable via the partially ordered set data-structure (the poset).
eSSA allows us to represent these orderings directly in the structure of the code. Here we take inspiration from the ABCD algorithm. In ABCD, the implementors eliminate bounds checks based on finding the shortest path through a graph based on an eSSA construction with constants appearing as weights. Since we have done range analysis before this point, constants can be propagated and we can fold those weights. Additionally, because the meet operator of phi nodes is defined as a max, whenever we encounter a value who's upper bound has been widened, we know that we can terminate the search for that particular subgraph.
drawbacks/challenges
Moving from a dominator-based constraint layering to dataflow solving has certain challenges. Instead of going from an infinite range down to a more specific one, we start from specific values and expand the range via arithmetic. This means we have to be much more careful about overflow and other arithmetic properties.
The prove pass has a bit of a reputation for being finnicky about which code constructions result in a bounds check being eliminated or not. While the new solver will hopefully cause more bounds checks to be eliminated, reasoning about which ones get eliminated can involve dynamic behavior during the solve that can be difficult to "see" through.
The time spent in the prove pass may increase slightly. With the techniques outlined above, the theoretical bound is visiting every value in a function twice compared to once with the old analysis. While avoiding the bookkeeping of the both the poset and limit undo stack will gain us some speed, eSSA construction and the extra visits will probably eat into those gains.
The DAG search of the poset goes from only considering values that have been explicitly added to the poset, to walking the unpruned CFG. While search can often terminate early, we may find that we need to employ memoization or a union-find data structure to achieve reasonable speeds.
Further reading
-
Speed and Precision in Range Analysis [link]
Paper describing a pure range analysis implementation. Of particular note: figure 5 showing various features
being enabled/disabled and their impact on compilation speed and precision.
-
ABCD: eliminating array bounds checks on demand [link]
The main inspiration for the new constraint system.
Proposal Details
Technically, this is an internal change and I don't think it requires a proposal, but it is pretty substantial and people have already offered valuable feedback, so sending it to a wider audience:
eSSA for go's prove pass
Go's prove pass has served us well over the years, but the dominator-based algorithm has some drawbacks:
constraints that are true over all incoming paths, but are not established in a dominator, get missed. The prototypical example of this is min/max, which we currently handle specially
but small variations in code construction can evade our pattern matching. For example, an equivalent min/max construction over a pointer:
The subsequent uses of x will not have any nil checks pruned (by the prove pass at least, we still catch this in late nilcheckelim)
Induction variables are handled specially. With SIMD variants of loops on the horizon, the constructions that we use for loop variables are liable to change and defeat our pattern matching.
We already have one special case solution for this in the form of the chunked iteration pattern matcher, but a more general solution would be preferable.
Values having multiple ranges at different times during the analysis makes either replacing them or tagging them with information for a subset of blocks difficult. The simplifyBlock step
handles some of these, but the replacements are written ad-hoc. Leveraging our opt pattern matching infrastructure could help us catch more cases. A recent example of this problem
is https://go.dev/cl/785801
For these reasons, I propose that we replace the dominator-based algorithm with a two-stage dataflow range analysis and bounds-check elimination procedure, centered around eSSA.
Extended SSA
Extended SSA (eSSA) is a form of SSA where uses in conditionals that denote a range or ordering get turned into new copies of said value. These copies can then serve as stand-ins for "Value x at execution point y". For us, this enables two things that help with running range analysis dataflow quickly:
The tradeoff is that this form needs to be constructed before we can run our analysis. The current prototype I have does this with linear time algorithms only and takes 24.8 microseconds on a function that takes 69.0 microseconds to run the entire prove pass on.
A bonus of these new copies: they have their own storage. Marking them, either via Aux or an array in Func, would allow for later pattern matching in a .rules file
An example of a
minfunction in eSSA form. Conventionally, the copies are sigma or pi operations. Here, we use single-arity phi nodes.Before eSSA conversion:
After eSSA conversion:
These values will then be incorporated into the dataflow, denoting that v12 is less than v8 (because the positive branch was taken) and v9 is less than or equal v7 (because the negative branch was taken). Phis with multiple predecessors combine these orderings and the range information they denote. v13 in the above example will be less than v8 and less than or equal v7.
Instead of using the poset data structure for checking whether constraints are consistent after a branch, we can now perform the depth-first search directly on the use-def chain, since it now encodes orderings. This avoids having to build the posets DAG and removes the need for checkpointing and restoring.
Range analysis
For range analysis, I propose that we use a dataflow solution to propagate range information. Usually, this requires as many dataflow passes over the CFG as the height of your lattice, and for range analysis, this would be infinite. We avoid some of this expense by employing 2 techniques.
Widening/narrowing
While doing our dataflow analysis, we might find the need to revisit a value. Consider the following code:
Which turns into the following eSSA code:
Here, we will focus on v8 and v18, two versions of our induction variable. During the initial stage of our solution, we will find v8 to have
[0,0]as a range (because v16 is yet to be visited). This value will flow through v18[0,0], v16[1,1]and then finally back to v8. If we naively update our range to the union of v7 and v16[0,1], we will find ourself revisiting this loop until our Less64 conditional restrains our range, visiting this loop 200 times.To solve this problem, we employ widening. Whenever we revisit a value, we'll inspect in which ways the bounds of our range grow. For our worked example, the second visit of v8 indicates a growing upper bound. With the initial state, the range will then come out to
[0,inf]. This will flow through the conditional at v10 and be narrowed to[0,199].In practice, this means that we will visit values twice. Once to initialize the base case or discover the growth of a variable, and once to propagate the widened value.
Note that
s(v21) in our example gets a similar treatment toi, progressing through v21[0,0], v13[1,1], v21[0,inf](because of widening), v13[-inf,inf](because of overflow) and then finally v21[-inf,inf]. Calculating the final value ofsis possible with a scalar evolution pass, but outside the scope of this proposal.Bias towards strongly connected components during solve
Solving dataflow systems relies on iterating over the CFG until a fixed point is reached. This can involve multiple passes over a CFG, where state is evaluated, just to find that no update needs to be done.
To reduce the runtime of the analysis, we will instead solve by strongly connected component (SCC). By iterating over an SCC until it reaches a fixed point, we avoid having to revisit any of the values later on in the solve. This also interacts advantageously with widening. A value that is found to be widened in both lower bound and upper bound may in actuality only grow in one bound. Whether we discover this is dependent on the order in which we visit values. Doing the analysis by SCC will give more conservative ranges to be propagated to other values.
SCCs in Go are roughly analogous to loops. Here we can use the loop nesting forest to guide our solve. When enqueuing a value for analysis, we use a priority queue indexed on the loop depth of its block. By processing outer loops first, we ensure that the initial conditions for inner loops are established before we try to solve them. Occasionally, an inner loop may expose a value to an outer loop, but because we've run growth analysis on the outer loop already, it is unlikely to change the established range of any values.
Note that our current loop nesting forest only handles reducible CFGs and when an irreducible CFG is found, the loop to SCC equivalence is broken. These irreducible CFGs can only be constructed using gotos and are exceedingly rare. For example, there is only one instance of such a CFG in the standard library, and it is in a non performance-sensitive spot. For the initial implementation, I intend to ignore SCCs in functions with irreducible control flow, but future work may include changing our loop nesting forest definition, or running a pass before prove which would make the control flow reducible.
Constraint system
Range analysis by itself is fairly limited about what it can do as far as eliminating bounds checks. Since the length of a slice is initially unknown and come from outside context (for example, a slice being passed as a parameter to a function), numerical methods can only do so much. The vast majority of bounds checks that are eliminated currently happen by finding a check unsatisfiable via the partially ordered set data-structure (the poset).
eSSA allows us to represent these orderings directly in the structure of the code. Here we take inspiration from the ABCD algorithm. In ABCD, the implementors eliminate bounds checks based on finding the shortest path through a graph based on an eSSA construction with constants appearing as weights. Since we have done range analysis before this point, constants can be propagated and we can fold those weights. Additionally, because the meet operator of phi nodes is defined as a max, whenever we encounter a value who's upper bound has been widened, we know that we can terminate the search for that particular subgraph.
drawbacks/challenges
Moving from a dominator-based constraint layering to dataflow solving has certain challenges. Instead of going from an infinite range down to a more specific one, we start from specific values and expand the range via arithmetic. This means we have to be much more careful about overflow and other arithmetic properties.
The prove pass has a bit of a reputation for being finnicky about which code constructions result in a bounds check being eliminated or not. While the new solver will hopefully cause more bounds checks to be eliminated, reasoning about which ones get eliminated can involve dynamic behavior during the solve that can be difficult to "see" through.
The time spent in the prove pass may increase slightly. With the techniques outlined above, the theoretical bound is visiting every value in a function twice compared to once with the old analysis. While avoiding the bookkeeping of the both the poset and limit undo stack will gain us some speed, eSSA construction and the extra visits will probably eat into those gains.
The DAG search of the poset goes from only considering values that have been explicitly added to the poset, to walking the unpruned CFG. While search can often terminate early, we may find that we need to employ memoization or a union-find data structure to achieve reasonable speeds.
Further reading
Speed and Precision in Range Analysis [link]
Paper describing a pure range analysis implementation. Of particular note: figure 5 showing various features
being enabled/disabled and their impact on compilation speed and precision.
ABCD: eliminating array bounds checks on demand [link]
The main inspiration for the new constraint system.