Final simple changes to the LSR

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