\environment fonts_env \environment lsr_env \startcomponent pipelining \chapter[sec:pipelining]{Loop Pipelining} \startsynopsis This section describes the future plans of implementing loop pipelining in Vericert, also called loop scheduling. This addresses the final major issue with Vericert, which is efficiently handling loops. \stopsynopsis Standard instruction scheduling only addresses parallelisation inside hyperblocks, which are linear sections of code. However, loops are often the most critical sections in code, and scheduling only addresses parallelisation within one iteration. Traditionally, loop pipelining is performed as part of the normal scheduling step in \HLS, as the scheduling algorithm can be generalised to support these new constraints. However, it becomes expensive to check the correctness of a scheduling algorithm that transforms the code in this many ways. It is better to separate loop pipelining into it's own translation pass which does a source-to-source translation of the code. The final result should be similar to performing the loop pipelining together with the scheduling. \section{Loop pipelining example} \startplacemarginfigure[location=here,reference={fig:pipelined-loop},title={Example of pipelining a loop.}] \startfloatcombination[nx=2,distance=10mm,align=middle] \startplacesubfigure[title={Simple loop containing an accumulation of values with an inter-iteration dependency.}] \startframedtext[frame=off,offset=none,width={0.6\textwidth}] \starthlC for (int i = 1; i < N; i++) { c1 = acc[i-1] * c; c2 = x[i] * y[i]; acc[i] = c1 + c2; } \stophlC \stopframedtext \stopplacesubfigure \startplacesubfigure[title={Pipelined loop reducing the number of dependencies inside of the loop.}] \startframedtext[frame=off,offset=none,width={0.6\textwidth}] \starthlC c1 = acc[0] * c; c2 = x[1] * y[1]; for (int i = 1; i < N-1; i++) { acc[i] = c1 + c2; c2 = x[i+1] * y[i+1]; c1 = acc[i+1] * c; } acc[N-1] = c1 + c2; \stophlC \stopframedtext \stopplacesubfigure \stopfloatcombination \stopplacemarginfigure \in{Figure}[fig:pipelined-loop] shows an example of \emph{software pipelining} of a loop which accumulates values and modifies an array. In \in{Figure}{a}[fig:pipelined-loop], the body of the loop cannot be scheduled in less than three cycles assuming that a load takes two clock cycles. However, after transforming the code into the pipelined version in \in{Figure}{b}[fig:pipelined-loop], the number of inter-iteration dependencies have been reduced by moving the store into the next iteration of the loop. This means that the body of the loop could now be scheduled in two clock cycles. The process of pipelining the loop by being resource constrained can be done purely as a source-to-source translation in software using iterative modulo scheduling~\cite[rau94_iterat_sched], followed by modulo variable expansion~\cite[lam88_softw_pipel]. The steps performed in the optimisation are the following: \startitemize[n] \item Calculate a minimum \II, which is the lowest possible \II\ based on the resources of the code inside of the loop and the distance and delay of inter-iteration dependencies. \item Perform modulo scheduling with an increasing \II\ until one is found that works. The scheduling is performed by adding instructions to a \MRT~\cite[lam88_softw_pipel], assigning operations to each resource for one iteration. \item Once a valid modulo schedule is found, the loop code can be generated from it. To keep the \II\ that was found in the previous step, modulo variable expansion might be necessary and require unrolling the loop. \stopitemize This is very similar to the way loop scheduling directly in hardware is performed, but it is often done at the same time as scheduling. \section{Verification of pipelining} Verification of pipelining has already been performed in CompCert by \cite[authoryears][tristan10_simpl_verif_valid_softw_pipel]. Assuming that one has a loop body $\mathcal{B}$, the pipelined code can be described using the prologue $\mathcal{P}$, the steady state $\mathcal{S}$, the epilogue $\mathcal{E}$, and finally some additional variables representing the minimum number of iterations that need to be performed to be able to use the pipelined loop $\mu$ and representing the unroll factor of the steady state $\delta$. The goal is to verify the equivalence of the original loop and the pipelined loop using a validation algorithm, and then prove that the validation algorithm is \emph{sound}, i.e. if it finds the two loops to be equivalent, this implies that they will behave the same according to the language semantics. Essentially, as the loop pipelining algorithm only modifies loops, it is enough to show that the input loop $X$ is equivalent to the pipelined version of the loop $Y$. Assuming that the validation algorithm is called $\alpha$, we therefore want to show that the following statement holds, where $X_N$ means that we are considering $N$ iterations of the loop. \placeformula\startformula \forall N,\quad \alpha(X_N) = \startmathcases \NC \alpha(Y_{N/\delta}; X_{N\%\delta}) \NC N \ge \mu \NR \NC \alpha(X_N) \NC \text{otherwise} \NR \stopmathcases\stopformula This states that for any number of iteration of the loop $X$, the formula should hold. As the number of loop iterations $N$ are not always known at compile time, this may become an infinite property that needs to be checked. This infinite property can be proven by checking smaller finite properties that loop pipelining should ensure. The two key insights by \cite[author][tristan10_simpl_verif_valid_softw_pipel] where that mainly only the two following properties needed to be checked: \placeformula[eq:loop1]\startformula \alpha(\mathcal{S}; \mathcal{E}) = \alpha(\mathcal{E}; \mathcal{B}^{\delta}) \stopformula \placeformula[eq:loop2]\startformula \alpha(\mathcal{P}; \mathcal{E}) = \alpha(\mathcal{B}^{\mu}) \stopformula \noindent The first property shown in \in{Equation}[eq:loop1] describes the fact that one can exit the loop at any point and execute $\mathcal{B}^{\delta}$ iterations of the loop instead of executing one more body $\mathcal{S}$ of the pipelined loop. The second property shown in \in{Equation}[eq:loop2] describes that executing the initial loop $\mu$ times is exactly the same as executing the prologue $\mathcal{P}$ of the loop followed by the epilogue $\mathcal{E}$. In addition to some simpler properties, this means that the infinite property can still be checked.\footnote{In addition to other more trivial properties, for example that the loop structure is correct, and only contains one increment operation on the induction variable.} Finally, the verifier itself needs to be proven correct, meaning the correctness of the symbolic evaluation needs to be shown to be semantics preserving. If the comparison between two symbolic states succeeds, then this must imply that the initial blocks themselves execute in the same way. \section{Novelties of verifying software pipelining in Vericert} As mentioned in the previous section, software pipelining has already been implemented in CompCert by \cite[author][tristan10_simpl_verif_valid_softw_pipel]. From an implementation point of view for the actual pipelining algorithm that was implemented was a backtracking iterative modulo scheduling algorithm paired with modulo variable expansion. However, the results were underwhelming because it was tested on an out-of-order PowerPC G5 processor, whereas pipelining is more effective on in-order processors to take full advantage of the static pipeline. In addition to that, alias analysis on memory dependencies is also not performed, which is perhaps the best way to improve the performance of the optimisation. Finally, the loop scheduling is also only performed on basic blocks, and not on extended basic blocks such as superblocks or hyperblocks. These are all short-comings that could be easily improved by using our existing {\sc RTLBlock} or {\sc RTLPar} language as the source language of the pipelining transformation. Paired with the scheduling step, one could extract more parallelism and also support conditionals in loop bodies. Memory aliasing is not directly supported yet in the {\sc RTLBlock} abstract interpretation, however, using some simple arithmetic properties it should be possible to normalise memory accesses and therefore prove reordering of memory accesses that do not alias under certain conditions. From a proof perspective there is also some improvements that can be made to the work. First of all, the proof from the paper was actually never fully completed: \startframedtext[ frame=off, leftframe=on, offset=0pt, loffset=0.5cm, framecolor=darkcyan, rulethickness=2pt, location=middle, width=\dimexpr \textwidth - 1cm \relax, ] {\noindent\it [Semantic preservation going from unrolled loops in a basic block representation to the actual loops in a CFG] is intuitively obvious but surprisingly tedious to formalize in full details: indeed, this is the only result in this paper that we have not yet mechanized in Coq.} \startalignment[flushright] --- \cite[alternative=authoryears,right={, Section 6.2}][tristan10_simpl_verif_valid_softw_pipel]. \stopalignment \stopframedtext \noindent The proof of semantic preservation going from unrolled loops with basic blocks back to a control-flow graph were tedious, showing that the language was not designed to handle loop transformations well. However, recent work on the formalisation of polyhedral transformations of loops~\cite[authoryear][courant21_verif_code_gener_polyh_model] shows that this may be a better representation for the intermediate language. However, translations to and from the {\sc Loop} language would still have to be implemented. In addition to that, the original loop-pipelining implementation did not have a syntactic representation of basic blocks, making the proofs a bit more tedious than necessary. This may mean that the current syntactic representation of basic blocks in {\sc RTLBlock} may simplify the translations as well. \section{Hardware and Software Pipelining} Hardware and software pipelining algorithms share many features, even though the final implementation of the pipeline is quite different. Pipelining in hardware is intuitive. If one has two separate blocks where one is data-dependent on the other, then it is natural to pass a new input to the first block as soon as it has finished and passed the result to the second block. This idea is also the key building block for processor designs, as it is a straightforward way to improve the throughput of a series of distinct and dependent operations. In \HLS\ it is also an important optimisation to efficiently translate loops. Loops are often the limiting factor of a design, and any improvements in their translation can reduce the throughput of the entire design. The \HLS\ tool therefore often automatically creates pipeline stages for loops and calculates a correct \II\ for the loop, which will be the rate at which the pipeline needs to be filled. The benefit of generating hardware directly, is that the pipeline can already be laid out in the optimal and natural way. It is less clear why, and especially how, software can be pipelined in the same way as hardware, and what the benefits are if the code is going to be executed.\footnote{It is more clear why scheduling would be important on a VLIW processor, but still not clear how the pipelined loop can be represented in software without explicit parallelism.} The main difference between to a hardware pipeline is that in software the code is executed inherently sequentially. This means that it is not possible to lay out a pipeline in the same way, as the next input cannot just be passed to the loop while it is executing. However, a pipeline can be simulated in software, so that it behaves the same as the hardware pipeline, but it will manually have to unroll and rearrange the loop body so that all the stages can be executed by following one control-flow. However, the order of instructions will be quite different hardware, where the pipeline can be written naturally in sequential order of the stages. In software, the pipeline is instead represented by one horizontal slice of the pipeline, which will be the new loop body and represents the computation that the whole hardware pipeline is performing at one point in time. The main question that comes up is are the two pipelining methods actually equivalent? In Vericert we are assuming that performing software pipelining, followed by scheduling and finally followed by the hardware generation approximates the hardware pipelining that traditional \HLS\ tools perform as part of their hardware generation. \startmode[chapter] \section{Bibliography} \placelistofpublications \stopmode \stopcomponent