From 29abf1b418989b544295e004a215c0e9cfb18280 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 6 May 2022 15:21:19 +0100 Subject: Final simple changes to the LSR --- chapters/conclusion.tex | 6 ++++++ chapters/schedule.tex | 13 +++++++++++-- chapters/scheduling.tex | 52 ++++++++++++++++++++++++++++++------------------- main.tex | 2 +- 4 files changed, 50 insertions(+), 23 deletions(-) diff --git a/chapters/conclusion.tex b/chapters/conclusion.tex index ee816cb..62779fc 100644 --- a/chapters/conclusion.tex +++ b/chapters/conclusion.tex @@ -5,4 +5,10 @@ \chapter{Conclusion} +Vericert is currently a fully verified but simple \HLS\ tool. For the rest of my PhD, the goal will +be to improve the throughput of the designs that are generated by Vericert, by first parallelising +instructions using scheduling on hyperblocks, as well as introducing modulo scheduling to handle +loops. One other possible extension could be to collaborate with Sandrine Blazy and Delphine +Demange to implement a dynamic \HLS\ tool using \GSA\ as a base representation. + \stopcomponent diff --git a/chapters/schedule.tex b/chapters/schedule.tex index d367e4b..c1bb4c3 100644 --- a/chapters/schedule.tex +++ b/chapters/schedule.tex @@ -108,11 +108,20 @@ slightly different structure of the program. \subsection{Starting Work on Modulo Scheduling} After the proofs about hyperblock scheduling are finished, a natural extension is to work on -implementing modulo scheduling, which entails rearranging instructions in loops. +implementing modulo scheduling, which entails rearranging instructions in loops. This would greatly +improve the performance of Vericert as a whole and it would be the final big HLS specific +optimisation that would need to be implemented to be able to call Vericert a proper HLS tool. +However, as mentioned by \cite[author][tristan10_simpl_verif_valid_softw_pipel], dealing with loops +in CompCert can be very tricky and could therefore be an interesting optimisation to work on but may +also be quite challenging. \subsection{Possible Implementation for Dynamic Scheduling} Another plausible extension to Vericert is adding dynamic scheduling, as an alternative, or in -addition to, static scheduling. +addition to, static scheduling. This would have a benefit of maybe being able to combine static and +dynamic scheduling within one design in a verified manner, which was shown to be effective by +\cite[authoryears][cheng20_combin_dynam_static_sched_high_level_synth], and would also be a good way +to improve the throughput of Vericert on loops that need to be scheduled, especially if these have +complicated memory dependencies that would not be analysed by modulo scheduling. \stopcomponent diff --git a/chapters/scheduling.tex b/chapters/scheduling.tex index dcbb409..916812c 100644 --- a/chapters/scheduling.tex +++ b/chapters/scheduling.tex @@ -287,16 +287,24 @@ language. However, instead of mapping from states to instructions, \rtlblock\ ma hyperblocks, and \rtlpar\ maps from states to parallel hyperblocks, which will be described in the next sections. -\placeformula[eq:standard] \startformula \startmathalignment -\NC i\ \ \colon\colon= \NC \ \ \text{\tt RBnop} \NR +\startplacefigure[location={here,none}] + \startfloatcombination[nx=2] + \startplacefigure[reference={eq:standard},title={Syntax for instructions within a hyperblock.}] + \startframedtext[frame=off,offset=none,width={0.45\textwidth}] + \startformula \startalign +\NC i\ \ \eqdef \NC \ \ \text{\tt RBnop} \NR \NC \NC |\ \ \text{\tt RBop}\ p?\ \mathit{op}\ \vec{r}\ d \NR \NC \NC |\ \ \text{\tt RBload}\ p?\ \mathit{chunk}\ \mathit{addr}\ \vec{r}\ d \NR \NC \NC |\ \ \text{\tt RBstore}\ p?\ \mathit{chunk}\ \mathit{addr}\ \vec{r}\ s \NR \NC \NC |\ \ \text{\tt RBsetpred}\ p?\ c\ \vec{r}\ d \NR -\stopmathalignment \stopformula +\stopalign \stopformula +\stopframedtext -\placeformula[eq:cf-instr] \startformula \startmathalignment -\NC i_{\mathit{cf}}\ \ \colon\colon= \NC \ \ \text{\tt RBcall}\ \mathit{sig}\ f\ \vec{r}\ d\ n \NR + \stopplacefigure + \startplacefigure[reference={eq:cf-instr},title={Control-flow instructions ending a hyperblock.}] +\startframedtext[frame=off,offset=none,width={0.45\textwidth}] + \startformula \startmathalignment +\NC i_{\mathit{cf}}\ \ \eqdef \NC \ \ \text{\tt RBcall}\ \mathit{sig}\ f\ \vec{r}\ d\ n \NR \NC \NC |\ \ \text{\tt RBtailcall}\ \mathit{sig}\ f\ \vec{r} \NR \NC \NC |\ \ \text{\tt RBbuiltin}\ f_{\mathit{ext}}\ \vec{r}\ r\ n \NR \NC \NC |\ \ \text{\tt RBcond}\ c\ \vec{r}\ n_{1}\ n_{2} \NR @@ -305,12 +313,16 @@ next sections. \NC \NC |\ \ \text{\tt RBgoto}\ n \NR \NC \NC |\ \ \text{\tt RBpred\_{cf}}\ P\ i_{\mathit{cf}_{1}}\ i_{\mathit{cf}_{2}} \NR \stopmathalignment \stopformula +\stopframedtext + \stopplacefigure + \stopfloatcombination +\stopplacefigure \rtlblock\ instructions are split into two types of instructions, standard instructions and control-flow instructions. The standard instructions are the instructions that can be placed into hyperblocks, whereas control-flow instructions are the instructions that can end hyperblocks. The -standard instructions are shown in \in{Equation}[eq:standard], whereas the control-flow instructions -are shown in \in{Equation}[eq:cf-instr]. Most instructions are quite similar to their \rtl\ +standard instructions are shown in \in{Figure}[eq:standard], whereas the control-flow instructions +are shown in \in{Figure}[eq:cf-instr]. Most instructions are quite similar to their \rtl\ counterparts, however, there are some instructions that have been added. \type{RBsetpred} is a standard instruction which sets a predicate equal to an evaluated condition. This instruction is used during if-conversion to set the predicate to the value of the condition in the conditional @@ -461,11 +473,11 @@ account. Any predicate can be replaced with an equivalent predicate. \stopitemize -The symbolic expressions have the following form: - \define\sep{\ |\ } -Resources: +\noindent The symbolic expressions have the following form: + +\noindent Resources: \startformula \rho\ \eqdef\ r \sep p \sep \text{\tt Mem} \stopformula @@ -530,18 +542,18 @@ predicated type and append the first predicated type to the second: \placeformula[eq:4]\startformula\startalign[n=1,align={1:left}] \NC \text{\tt r1} = \startcases - \NC \mono{r1}^{0} + \mono{r4}^{0} + \mono{r4}^{0}, \quad \NC \mono{p1} \NR - \NC \mono{r1}^{0}, \quad \NC \mono{!p1} \NR + \NC \text{\tt r1}^{0} + \text{\tt r4}^{0} + \text{\tt r4}^{0}, \quad \NC \text{\tt p1} \NR + \NC \text{\tt r1}^{0}, \quad \NC \text{\tt !p1} \NR \stopcases \NR -\NC \mono{r2} = \mono{r1}^{0} + \mono{r4}^{0}\NR -\NC\mono{r3} = +\NC \text{\tt r2} = \text{\tt r1}^{0} + \text{\tt r4}^{0}\NR +\NC\text{\tt r3} = \startcases - \NC \left( \mono{r1}^{0} \times \mono{r1}^{0} \right) \times \left( \mono{r1}^{0} \times - \mono{r1}^{0} \right),\quad \NC \mono{!p2 \&\& !p1} \NR - \NC \mono{r1}^{0} \times \mono{r4}^{0},\quad \NC \mono{p2 \&\& !p1} \NR - \NC \left( \mono{r1}^{0} + \mono{r4}^{0} + \mono{r4}^{0} \right) \times \mono{r4}^{0},\quad - \NC \mono{!p2 \&\& p1}\NR - \NC \mono{r3}^{0} \times \mono{r3}^{0},\quad \NC\mono{p2 \&\& p1}\NR + \NC \left( \text{\tt r1}^{0} \times \text{\tt r1}^{0} \right) \times \left( \text{\tt r1}^{0} \times + \text{\tt r1}^{0} \right),\quad \NC \text{\tt !p2 \&\& !p1} \NR + \NC \text{\tt r1}^{0} \times \text{\tt r4}^{0},\quad \NC \text{\tt p2 \&\& !p1} \NR + \NC \left( \text{\tt r1}^{0} + \text{\tt r4}^{0} + \text{\tt r4}^{0} \right) \times \text{\tt r4}^{0},\quad + \NC \text{\tt !p2 \&\& p1}\NR + \NC \text{\tt r3}^{0} \times \text{\tt r3}^{0},\quad \NC\text{\tt p2 \&\& p1}\NR \stopcases\NR \stopalign \stopformula diff --git a/main.tex b/main.tex index 7bffd10..605809d 100644 --- a/main.tex +++ b/main.tex @@ -33,7 +33,7 @@ \component pipelining %\component dynamic \component schedule - %\component conclusion + \component conclusion \stopbodymatter \startbackmatter -- cgit