1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
\environment fonts_env
\environment lsr_env
\startcomponent schedule
\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] 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 ongoing.
\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
\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.
\startplacemarginfigure[
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},
]
\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
\stopplacemarginfigure
\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 generate 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. 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. 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
|
