A Paper a Decade #16: A simple, verified validator for software pipelining
What a decade since I’ve last posted about a paper I read. I have since gotten to work on compilers, so I’ve read this paper out of more than idle curiosity.
The paper starts out by explaining what software pipelining / Modulo Scheduling is. One point of definitional confusion is that it appears to actually be presenting the Modulo Variable Expansion1 algorithm rather than vanilla Modulo Scheduling (which is a special case of MVE).
Then it defines the problem by introducing fancy variables to say “for every iteration count, the result of the pipelined and the original loop should be the same”:
- \(\mathcal{S}\) is the new loop body […]
- \(\mathcal{P}\) is the loop prolog […]
- \(\mathcal{E}\) is the loop epilog […]
- \(\mu\) is the minimum number of iterations that must be performed to be able to use the pipelined loop.
- \(\delta\) is the amount of unrolling that has been performed […]
[…]
Likewise, the generated code behaves either like \(\mathcal{B}^N\) if \(N < \mu\), or like
\[\mathcal{P};\mathcal{S}^{\kappa(N)};\mathcal{E};\mathcal{B}^{\rho(N)}\]
if \(N \geq \mu\), where
\[ \begin{aligned} \kappa(N) &\overset{\text{def}}{=} (N - \mu)/\delta \\ \rho(N) &\overset{\text{def}}{=} N - \mu - \delta \times \kappa(N) \end{aligned} \]
The verification problem therefore reduces to establishing that, for all \(N\), the two basic blocks
\[ X_N \overset{\text{def}}{=} \mathcal{B}^N \qquad\text{and}\qquad Y_N \overset{\text{def}}{=} \mathcal{P};\mathcal{S}^{\kappa(N)};\mathcal{E};\mathcal{B}^{\rho(N)} \tag{1}\]
are semantically equivalent.
Here, \(N\) is the trip count, \(\alpha\) is the result of symbolic execution, and \(\mathcal{B}\) is the original, single basic-block loop body.
Nice. Now if we could just \(\forall N\). But there are countably too many of those to symbolically execute, so let’s read on.
The key discovery of this paper is that this undecidable property \(\forall N,\ \alpha(X_N) = \alpha(Y_N)\) is implied by (and, in practice, equivalent to) the following two decidable conditions:
\[\alpha(\mathcal{E};\mathcal{B}^{\delta}) = \alpha(\mathcal{S};\mathcal{E})\]
\[\alpha(\mathcal{B}^{\mu}) = \alpha(\mathcal{P};\mathcal{E})\]
In essence: exiting the pipelined loop and running the original loop body (\(\delta\) times if it was unrolled) should be the same as continuing it and exiting. You throw in some conditions about the induction variable and the loop bound, and you have the algorithm in section 5.
That is the core insight of the paper. The rest of it concerns itself with their symbolic execution method, the proof, and some caveats about the approach.
The interesting one is that passing the validation condition is sufficient but not necessary for the transformation being correct (i.e. being equivalent to Equation 1). The paper says they “strongly believe it holds in practice as long as the software pipelining algorithm used is purely syntactic”. Which is a somewhat unsatisfactory thing to say in a theoretical CS paper, but it sounds reasonable.
They implemented a software pipeliner and this validator for CompCert, and have not found it to reject correct transformations, which gives this claim a bit of empirical weight.
The rest of the caveats are pretty much classic caveats to any symbolic execution technique.
I hope to get a chance to implement this, and the fact that software pipelining algorithms are usually purely syntactic makes the job easier: from a very high level, we are comparing terms of def-use chains.
Read the paper here.