\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 its 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 sufficient 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] were 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{This is 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, 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, although this is perhaps the best way to improve the results 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 are 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 was 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 clearer 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 in 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. \subsection{Hardware Pipelining Can be Approximated by Software Pipelining} The hope is that hardware pipelining can be approximated by software pipelining, so that the translation can easily be separated. We argue that this is in fact possible, with two additional properties that can be added to the software intermediate language. The main two problems that software pipelining runs into when directly comparing it to the equivalent hardware pipeline are first the duplicated code for the prologue and the epilogue, and secondly the possible loop unrolling that is necessary to then allocate the registers correctly. \paragraph{Removing duplicate prologue and epilogue.} Disregarding the code duplication that results from generating the prologue and the epilogue, the main problem with having these pieces of code is that one ends up with a loop that has a minimum number of iterations which it needs to be executed for. This is not the case with a hardware pipeline, and it means that in software, to keep the code correct, the original version of the loop needs to be kept around so that if the iterations are under the minimum number of iterations the loop can execute, it will branch to the original loop instead. This does not really affect the performance of the code, but it does add a duplicate of every loop to the program, which might increase the size of the hardware dramatically. Predicated execution can be used to selectively turn on instructions that should be running at this point in time, therefore simulating the prologue and epilogue without having to duplicate any code. \paragraph{Removing the need to unroll the loop.} In addition to that, sometimes register allocation will require the loop to be unrolled many times to remain correct. This also means that the original loop will have to be kept around in case the number of executions of the loop is not divisible by the number of times the loop was unrolled. However, by using a rotating register file~\cite[rau92_regis_alloc_softw_pipel_loops] the clash between registers from different iterations is removed, thereby eliminating the need for register allocation. This does increase the amount of registers, however, this can further be optimised. In addition to that, rotating register files act a lot like proper hardware registers in pipelines. \startmode[chapter] \section{Bibliography} \placelistofpublications \stopmode \stopcomponent