Save liveness results for DestinationPropagation

[cjgillot]

DestinationPropagation needs to verify that merge candidates do not conflict with each other. This is done by verifying that a local is not live when its counterpart is written to.

To get the liveness information, the pass runs MaybeLiveLocals dataflow analysis repeatedly, once for each propagation round. This is quite costly, and the main driver for the perf impact on ucd and diesel. (See #115105 (comment))

In order to mitigate this cost, this PR proposes to save the result of the analysis into a SparseIntervalMatrix, and mirror merges of locals into that matrix: liveness(destination) := liveness(destination) union liveness(source).

Proof

We denote by ' all the quantities of the transformed program. Let $\varphi$ be a mapping of locals, which maps source to destination, and is identity otherwise. The exact liveness set after a statement is $out'(statement)$, and the proposed liveness set is $\varphi(out(statement))$.

Consider a statement. Suppose that the output state verifies $out' \subset phi(out)$. We want to prove that $in' \subset \varphi(in)$ where $in = (out - kill) \cup gen$, and conclude by induction.

We have 2 cases: either that statement is kept with locals renumbered by $\varphi$, or it is a tautological assignment and it removed.

1. If the statement is kept: the gen-set and the kill-set of $statement' = \varphi(statement)$ are $gen' = \varphi(gen)$ and $kill' = \varphi(kill)$ exactly.
   From soundness requirement 3, $\varphi(in)$ is disjoint from $\varphi(kill)$.
   This implies that $\varphi(out - kill)$ is disjoint from $\varphi(kill)$, and so $\varphi(out - kill) = \varphi(out) - \varphi(kill)$. Then $\varphi(in) = (\varphi(out) - \varphi(kill)) \cup \varphi(gen) = (\varphi(out) - kill') \cup gen'$.
   We can conclude that $out' \subset \varphi(out) \implies in' \subset \varphi(in)$.

2. If the statement is removed. As $\varphi(statement)$ is a tautological assignment, we know that $\varphi(gen) = \varphi(kill) = \{ destination \}$, while $gen' = kill' = \emptyset$. So $\varphi(in) = \varphi(out) \cup \{ destination \}$. Then $in' = out' \subset out \subset \varphi(in)$.

By recursion, we can conclude by that $in' \subset \varphi(in)$ everywhere.

This approximate liveness results is only suboptimal if there are locals that fully disappear from the CFG due to an assignment cycle. These cases are quite unlikely, so we do not bother with them.

This change allows to reduce the perf impact of DestinationPropagation by half on diesel and ucd (#115105 (comment)).

cc @JakobDegen

[rustbot]

r? @jackh726

(rustbot has picked a reviewer for you, use r? to override)

[rustbot]

Some changes occurred to MIR optimizations

cc @rust-lang/wg-mir-opt

[JakobDegen]

I don't exactly buy the proof. The induction on the proof seems to be in reverse graph structure; it's missing the component that reasons across basic blocks - but trying to add this component in won't work nicely, because the induction will fail on backedges.

That being said, I don't think the algorithm is actually wrong, and we can make it in a more straightforward manner: Instead of talking about merging locals, let's pretend that we removed the old locals S and T, and replaced them with a new local, U. Imagine for the same of contradiction that there was a location L at which U is live but neither of S or T were; without loss of generatlity, let the later use which causes U to be live have been a use of S pre-transformation. Consider the sequence of executed statements that begins at L and ends at the later use which causes U to be live. By the correctness (and some additional properties) of the transformation, there also existed a pre-transformation execution of the program along that same sequence of statements. So how is it that S was not live at L pre-transformation? There must have been an assignment to S which was removed during the transformation. But the only possible such assignment is S = T, and this punts the problem over to asking how T might have been not-live.

[cjgillot]

I don't exactly buy the proof. The induction on the proof seems to be in reverse graph structure; it's missing the component that reasons across basic blocks - but trying to add this component in won't work nicely, because the induction will fail on backedges.

The induction is one the dataflow fixed-point iteration. I don't need to specialize for backedges.

For back-edges, consider the exact dataflow equation $out' = \bigcup in'(successors)$. We have $\varphi(out) = \bigcup \varphi(in(successors))$.
If all successors verify $in'(successor) \subset \varphi(in(successor))$, we have $out' \subset \varphi(out)$.

[jackh726]

Can we r? @JakobDegen

I unfortunately don't have the background to review this properly right now, nor the time atm to learn that background.

[cjgillot]

@JakobDegen I'm not sure how to read your review. Is this good to merge, or do you need me to make some changes?

[bors]

☔ The latest upstream changes (presumably #113218) made this pull request unmergeable. Please resolve the merge conflicts.

[wesleywiser]

@JakobDegen could you clarify if you would like to see any additional changes made to this PR? Thanks! 🙂

[lqd]

Factoring out LivenessValues has tension in that rustc_borrowck depends on its internals at the very least for MIR dumps.

[bors]

☔ The latest upstream changes (presumably #118143) made this pull request unmergeable. Please resolve the merge conflicts.

[lqd]

Btw @cjgillot I'm not sure it'd be super useful to you but if you needed to make some progress here, I'd gladly r+ a PR about the rustc_borrowck refactorings, modulo the LivenessValues changes and what I said in this comment -- and leave the dataflow proof clarification to Jakob.

[bors]

☔ The latest upstream changes (presumably #117880) made this pull request unmergeable. Please resolve the merge conflicts.

[apiraino]

Switching to waiting on author to reply to unresolved comments. Feel free to request a review with @rustbot ready, thanks.

@rustbot author

[cjgillot]

r? wg-mir-opt

[oli-obk]

I think this should stay assigned to @JakobDegen as I won't be able to give it the kind of detailed review this pass needs

r? @JakobDegen

[cjgillot]

Discussed with @JakobDegen on zulip.
@bors r=JakobDegen rollup

[bors]

📌 Commit 1d6723a has been approved by JakobDegen

It is now in the queue for this repository.