1 files changed, 117 insertions, 1 deletions
diff --git a/chapters/schedule.tex b/chapters/schedule.tex
index 9dc8d38..1711108 100644
--- a/chapters/schedule.tex
+++ b/chapters/schedule.tex
@@ -1 +1,117 @@
-\chapter{Schedule}
+\environment fonts_env
+\environment lsr_env
+
+\startcomponent pipelining
+
+\definecolor[hyperblockcolour][x=66C2A5]
+\definecolor[dynamiccolour][x=FC8D62]
+\definecolor[modulocolour][x=8DA0CB]
+\definecolor[thesiscolour][x=E78AC3]
+
+\chapter[sec:schedule]{Schedule}
+
+The structure of the thesis has been described in the previous chapters.  Out of these chapters, the
+work for \in{Chapter}[sec:hls] has been completed, the work for \in{Chapter}[sec:scheduling] is
+still ongoing and finally the work in \in{Chapter}[sec:pipelining] and \in{Chapter}[sec:dynamic] has
+not been started yet.  This chapter will describe how the rest of the work will be completed.  The
+current plan is to finish all the work including the thesis by June 2023, which is when the funding
+will run out.
+
+\section{Timeline}
+
+The main timeline for the rest of the PhD is shown in \in{Figure}[fig:future-gantt].  It is split
+into four main sections:
+
+\desc{Hyperblock scheduling} The first section describes the work that is currently going on about
+hyperblock scheduling, and is described in \in{Chapter}[sec:scheduling].  Currently, the main proofs
+need to be completed, as well as submitting a paper about the work to FMCAD/POPL/PLDI.  In general,
+this work was supposed to be finished in November 2021, however, due to complications with the
+actual formulation of the semantics, as well as the number of proofs that need to be completed, the
+work is still on going.
+
+\desc{Modulo scheduling} The second piece of work is described in \in{Chapter}[sec:pipelining] and
+describes the implementation of modulo scheduling to perform scheduling on loops.  This work will be
+based on existing work by \cite[alternative=authoryears][tristan10_simpl_verif_valid_softw_pipel].
+However, it is worth noting that the proof by
+\cite[alternative=author][tristan10_simpl_verif_valid_softw_pipel] does include parts that are not
+completely verified in Coq, meaning there may be various improvements that could be done to the
+proof.
+
+\desc{Dynamic scheduling} Dynamic scheduling is another route that could be explored by using
+Vericert to pass through \SSA, as well as GSA, and finally generate dynamic HTL (or some other
+similar hardware language).  During my visit at Inria Rennes, I worked with Sandrine Blazy and
+Delphine Demange to extend CompCertSSA~\cite[barthe14_formal_verif_ssa_based_middl_end_compc] with
+\infull{GSA} (\GSA)~\cite[ottenstein90_progr_depen_web].  Not only should this allow for global
+optimisations of \SSA\ code, but it should also allow for a more straightforward translation to
+hardware as the GSA code can just be viewed as a \DFG.  Instead of working on modulo scheduling, it
+could therefore be interesting to work on a formally verified dynamic scheduling translation.
+
+\startplacefigure[
+  title={Gantt chart describing the future plan for 2022 and 2023.  The main funding runs out
+    mid-2023, so the plan is to finish the thesis writing by then as well.},
+  reference={fig:future-gantt},
+  location=top,
+]
+  \hbox{\startgantt[xunitlength=17.5mm]{15}{6}
+    \startganttitle
+      \numtitle{2022}{1}{2022}{4}
+      \numtitle{2023}{1}{2023}{2}
+    \stopganttitle
+    \startganttitle
+      \numtitle{1}{1}{4}{1}
+      \numtitle{1}{1}{2}{1}
+    \stopganttitle
+    \ganttgroup{\rmx Hyperblock Scheduling}{0}{3}
+    \ganttbar[color=hyperblockcolour]{\rmx Proof}{0}{2}
+    \ganttbarcon[color=hyperblockcolour]{\rmx Paper Submission}{2}{1}
+    \ganttgroup{\rmx Modulo Scheduling}{2}{3}
+    \ganttbar[color=modulocolour]{\rmx Implementation}{2}{1}
+    \ganttbarcon[color=modulocolour]{\rmx Proof}{3}{2}
+    \ganttgroup{\rmx Dynamic Scheduling}{0}{5}
+    \ganttbar[color=dynamiccolour]{\rmx RTL $\rightarrow$ GSA}{0}{1}
+    \ganttbarcon[color=dynamiccolour]{\rmx GSA $\rightarrow$ RTL}{1}{1}
+    \ganttbar[color=dynamiccolour]{\rmx GSA $\rightarrow$ HTL}{2}{3}
+    \ganttcon{1}{9}{2}{11}
+    \ganttgroup{\rmx Thesis}{4}{2}
+    \ganttbar[color=thesiscolour]{\rmx Thesis Writing}{4}{2}
+  \stopgantt}
+\stopplacefigure
+
+\section{Detailed Work Plan}
+
+This section describes a more detailed work plan for finalising the thesis.  First I will describe
+what the current plan is to finish the short term work of proving hyperblock scheduling, followed by
+a plan of either tackling dynamic scheduling or modulo scheduling.
+
+\subsection{Finishing Work on Hyperblock Scheduling}
+
+As described in \in{Chapter}{sec:scheduling}, the current milestone that needs to be achieved is
+proving hyperblock scheduling.  This requires proofs of the following translations:
+
+\desc{\sc RTL $\rightarrow$ RTLBlock} This translation generates basic blocks to ease the scheduling
+proof as well as simplify the scheduling algorithm.
+
+\desc{\sc IfConv} The {\sc IfConv} transformation introduces predicate instructions by conversing
+conditional statements.  This is necessary to generates hyperblocks and therefore improve the
+schedule by passing larger blocks to the scheduler.
+
+\desc{\sc RTLBlock $\rightarrow$ RTLPar} The proof of the scheduling algorithm itself, which is
+performed by validating the schedule and verifying that the validator is sound.
+
+\desc{\sc RTLPar $\rightarrow$ HTL} This translation generates the hardware from the parallel
+description of the schedule, which can then be translated to Verilog using an existing translation.
+As a translation from RTL to HTL has already been proven correct, it should be possible to reuse
+many proofs from that translation and only have to modify the top-level proofs that deal with the
+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.
+
+\subsection{Possible Implementation for Dynamic Scheduling}
+
+Another plausible extension to Vericert is adding dynamic scheduling, as an alternative, or in
+addition to, static scheduling.
+
+\stopcomponent