Update on Overleaf.

2 files changed, 104 insertions, 94 deletions

diff --git a/sketches/cfg_sketch.key b/sketches/cfg_sketch.key
index c7e1b5f..c7e1b5f 100755..100644
--- a/sketches/cfg_sketch.key
+++ b/sketches/cfg_sketch.key
diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index 2b9c6da..9470a18 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -5,10 +5,11 @@
 \usepackage{subcaption}
 \usepackage{tikz-timing}
 \usetikzlibrary{fit}
+\usetikzlibrary{decorations.pathreplacing}
 
 \usepackage{listings}
 \lstset{
-basicstyle=\tt\footnotesize,
+basicstyle=\tt,
 columns=fixed, basewidth=0.5em, %tip from https://tex.stackexchange.com/a/179072
 escapeinside=||,
 }
@@ -101,20 +102,70 @@ Introduced by \citet{Herklotz2020}, Vericert is a verified C-to-Verilog HLS tool
 
 Vericert branches off from CompCert at the intermediate language called \emph{register-transfer language} (RTL). Since that abbreviation is usually used in the hardware community for `register-transfer level', we shall henceforth avoid possible confusion by referring to the CompCert intermediate language as `3AC' (for `three-address code').
 
-In the 3AC language, each function in the program is represented as a numbered list of instructions with gotos -- essentially, a control-flow graph (CFG). The essence of Vericert's compilation strategy is to treat this CFG as a finite-state machine (FSM), with each instruction in the CFG becoming an FSM state, and each edge in the CFG becoming an FSM transition. Moreover, program variables that do not have their address taken are mapped to hardware registers; other variables (including arrays and structs) are allocated in a block of RAM that represents the stack. More precisely, Vericert builds a finite-state machine with datapath (FSMD)~\cite{HwangVahid1999}. An FSMD comprises two maps, both of which take the current FSM state as their input: the \emph{control logic} map for determining the next FSM state, and a \emph{datapath} map for updating the RAM and registers. FSMDs are captured in Vericert's new intermediate language, HTL. When Vericert compiles from HTL to the final Verilog output, these maps are converted from proper `mathematical' functions into syntactic Verilog case-statements, and each is placed inside an always-block.
+In the 3AC language, each function in the program is represented as a numbered list of instructions with gotos -- essentially, a control-flow graph (CFG). The essence of Vericert's compilation strategy is to treat this CFG as a state machine, with each instruction in the CFG becoming a state, and each edge in the CFG becoming a transition. Moreover, program variables that do not have their address taken are mapped to hardware registers; other variables (including arrays and structs) are allocated in a block of RAM that represents the stack. More precisely, Vericert builds a state machine with datapath~\cite{HwangVahid1999}. This comprises two maps, both of which take the current state as their input: the \emph{control logic} map for determining the next state, and a \emph{datapath} map for updating the RAM and registers. These state machines are captured in Vericert's new intermediate language, HTL. When Vericert compiles from HTL to the final Verilog output, these maps are converted from proper `mathematical' functions into syntactic Verilog case-statements, and each is placed inside an always-block.
+
+\begin{figure}
+\begin{tikzpicture}[yscale=-1]
+\node(fun1) at (1.5,2) {function};
+\node(fun2) at (0,2) {function};
+\node[anchor=west](C) at (-2,2) {\bf C:};
+\node(CFG1) at (1.5,3) {CFG};
+\node(CFG2) at (0,3) {CFG};
+\node(CFG) at (0.75,4) {CFG};
+\node[anchor=west](TAC) at (-2,3) {\bf 3AC:};
+\node(FSMD) at (0.75,5) {state machine};
+\node[anchor=west](HTL) at (-2,5) {\bf HTL:};
+\node(module) at (0.75,6) {module};
+\node[anchor=west](Verilog) at (-2,6) {\bf Verilog:};
+\draw[->] (fun1) to node [auto] {CompCert frontend} (CFG1);
+\draw[->] (fun2) to (CFG2);
+\draw[->] (CFG1) to node [auto, pos=0.2] {inlining} (CFG);
+\draw[->] (CFG2) to (CFG);
+\draw[->] (CFG) to node [auto] {state machine generation} (FSMD);
+\draw[->] (FSMD) to node [auto] {Verilog generation} (module);
+\end{tikzpicture}
+\caption{Key compilation passes and intermediate languages in Vericert~\cite{vericert}}
+\label{fig:vericert_flow}
+
+\begin{tikzpicture}[yscale=-1]
+\node(fun1) at (2,2) {function};
+\node(fun2) at (0,2) {function};
+\node[anchor=west](C) at (-2,2) {\bf C:};
+\node(CFG1) at (2,3) {CFG};
+\node(CFG2) at (0,3) {CFG};
+\node[anchor=west](TAC) at (-2,3) {\bf 3AC:};
+\node(FSMD1) at (2,4) {state machine};
+\node(FSMD2) at (0,4) {state machine};
+\node(FSMD3) at (2,5) {state machine};
+\node(FSMD4) at (0,5) {state machine};
+\node[anchor=west](HTL) at (-2,4) {\bf HTL:};
+\node(module) at (1,6) {module};
+\node[anchor=west](Verilog) at (-2,6) {\bf Verilog:};
+\draw[->] (fun1) to node [auto] {CompCert frontend} (CFG1);
+\draw[->] (fun2) to (CFG2);
+\draw[->] (CFG1) to node [auto] {state machine generation} (FSMD1);
+\draw[->] (CFG2) to (FSMD2);
+\draw[->, dashed] (FSMD1) to node [auto] {renaming} (FSMD3);
+\draw[->, dashed] (FSMD2) to (FSMD4);
+\draw[->, dashed] (FSMD3) to node [auto, pos=0.2] {Verilog generation} (module);
+\draw[->, dashed] (FSMD4) to (module);
+\end{tikzpicture}
+\caption{Key compilation passes and intermediate languages in Vericert-Fun, with dashed arrows indicating passes that have been implemented but not verified}
+\label{fig:vericert-fun_flow}
+\end{figure}
 
 \section{Implementation of Vericert-Fun}
 
 \tikzset{
-st/.style={draw=black, fill=white, rounded corners, align=left, font=\tt\footnotesize, minimum width=40mm},
+st/.style={draw=black, fill=white, rounded corners, align=left, font=\tt, minimum width=40mm},
 ed/.style={draw, ->},
 exted/.style={draw, thick, dotted, ->, rounded corners},
 lab/.style={anchor=south west, inner sep=1pt, font=\tiny},
-tit/.style={anchor=north west, font=\tt\footnotesize},
-edlab/.style={auto, inner sep=2pt, align=left, font=\tt\footnotesize}
+tit/.style={anchor=north west, font=\tt},
+edlab/.style={auto, inner sep=2pt, align=left, font=\tt}
 }
 
-Figure~\ref{fig:example_C} shows a simple C file that we shall employ as a worked example.
+Figure~\ref{fig:example_C} shows a simple C file that we shall employ as a worked example. Each instruction is colour-coded so it can be tracked through the compilation stages.
 
 \begin{figure}
 \centering
@@ -130,11 +181,11 @@ int main() {
   |\HL4{return v;}|
 }
 \end{lstlisting}
-\caption{Example C file}
+\caption{Running example: C program}
 \label{fig:example_C}
 \end{figure}
 
-Figure~\ref{fig:example_3AC} shows the 3AC that the CompCert frontend obtains from the C program in Fig.~\ref{fig:example_C}. Highlighting is used to show the correspondence between C instructions and 3AC instructions. \JW{In the HTL, the parameters to add are called a and b, but in the 3AC they're called x2 and x1. Presumably the HTL should use x2 and x1 too, right?}\YH{Yes, I definitely agree}
+Figure~\ref{fig:example_3AC} shows the 3AC representation of that C program, as obtained by the CompCert frontend. It takes the form of two CFGs, one per function. The control flow in this example is straightforward, but in general, 3AC programs can contain unrestricted gotos. The nodes of the CFGs are numbered in reverse order, as are the parameters of the \lstinline{add} function; both are conventions inherited from CompCert.
 
 \begin{figure}
 % \begin{lstlisting}
@@ -158,8 +209,8 @@ Figure~\ref{fig:example_3AC} shows the 3AC that the CompCert frontend obtains fr
 \node[st, fill=highlight5]    (a2) at (0,-1) {x3 = x2 + x1 + 0 (int)};
 \node[st, fill=highlight5, below=of a2] (a1) {return x3};
 \draw[ed] (a2) to (a1);
-\node[tit] at (-2.4,-0.2) (labmain) {add(x2, x1) \{};
-\node[tit] at (-2.4,-1.9) (labmain2) {\}};
+\node[tit] at ([xshift=-4mm, yshift=5mm]a2.north west) (labadd) {add(x2, x1) \{};
+\node[tit] at ([xshift=-4mm, yshift=-1mm]a1.south west) (labadd2) {\}};
 \begin{scope}[yshift=-24mm]
 \node[st, fill=highlight1]    (m9) at (0,-1) {x3 = 0};
 \node[st, fill=highlight2, below=of m9] (m8) {x6 = 1};
@@ -178,34 +229,19 @@ Figure~\ref{fig:example_3AC} shows the 3AC that the CompCert frontend obtains fr
 \draw[ed] (m4) to (m3);
 \draw[ed] (m3) to (m2);
 \draw[ed] (m2) to (m1);
-\node[tit] at (-2.4,-0.2) (labadd) {main() \{};
-\node[tit] at (-2.4,-6.1) (labadd2) {\}};
+\node[tit] at ([xshift=-4mm, yshift=5mm]m9.north west) (labmain) {main() \{};
+\node[tit] at ([xshift=-4mm, yshift=-1mm]m1.south west) (labmain2) {\}};
 \end{scope}
+\foreach\i in {1,2,...,9}
+  \node[lab, anchor=south east] at (m\i.west) {\i};
+\foreach\i in {1,2}
+  \node[lab, anchor=south east] at (a\i.west) {\i};
 \end{tikzpicture}
-\caption{Example CFG}
+\caption{Running example: 3AC representation comprising two CFGs}
 \label{fig:example_3AC}
 \end{figure}
 
-
-\begin{figure}
-\begin{tikztimingtable}[timing/d/background/.style={fill=white}, timing/xunit=1em]
-{\tt\small clk} & 0.5L 38{0.5C} \\
-{\tt\small rst} & 0.5H 19L \\
-{\tt\small fin} & 0.5X 17L H L \\
-{\tt\small state} & 0.5X D{9} D{8} D{7} 4D{12} D{6} D{5} D{4} 4D{10} D{3} D{2} D{1} 2D{11} \\
-{\tt\small add\_rst} & 3.5X H 6L H 8L \\
-{\tt\small add\_fin} & 4.5X 2L H 6L H 5L \\
-{\tt\small add\_state} & 4.5X D{2} D{1} 5D{3} D{2} D{1} 6D{3} \\
-\extracode
-\foreach\i in {1,2,...,19}
-\node[help lines, anchor=west, inner sep=0] at (\i-0.5,2.25) {\tiny \i};
-\begin{pgfonlayer}{background}
-  \vertlines[help lines]{0.5,1.5,...,18.5}
-\end{pgfonlayer}
-\end{tikztimingtable}
-\caption{Timing diagram}
-\label{fig:timingdiagram}
-\end{figure}
+Figure~\ref{fig:example_HTL} depicts the result of converting those CFGs into two state machines. The conversion of 3AC instructions into Verilog instructions has been described already by \citeauthor{vericert}; what is new here is the handling of function calls, so the following description concentrates on that aspect. Before we proceed, there are three conventions worth noting: first, ``$*{\rightarrow}\langle\mathit{node}\rangle$'' should be interpreted as an abbreviation for edges from all nodes to $\langle\mathit{node}\rangle$; second, the dotted edges are intended to suggest how control is passed between the two state machines, but they carry no formal meaning; and third, we allow the \lstinline{main} machine to register $\langle\mathit{reg}\rangle$ in the \lstinline{add} machine using ``\lstinline{add.}$\langle\mathit{reg}\rangle$''.
 
 \definecolor{background}{HTML}{eeeeee}
 \begin{figure}
@@ -254,13 +290,13 @@ Figure~\ref{fig:example_3AC} shows the 3AC that the CompCert frontend obtains fr
 \draw[ed] (ast2.north) to[bend right] node[edlab, swap] {rst} (a2.east);
 
 \coordinate (nw1) at ([xshift=-3mm, yshift=6mm]m9.north west); 
-\coordinate (se1) at ([xshift=13mm, yshift=-4mm]m11.south east);
+\coordinate (se1) at ([xshift=16mm, yshift=-4mm]m11.south east);
 \begin{pgfonlayer}{background}
 \node[draw, fill=background, rounded corners, fit=(nw1)(se1)] (main) {};
 \end{pgfonlayer}
 \node[tit, above=2mm of m9] (labmain) {\bfseries main()};
 \coordinate (nw2) at ([xshift=-3mm, yshift=6mm]a2.north west); 
-\coordinate (se2) at ([xshift=13mm, yshift=-4mm]a3.south east);
+\coordinate (se2) at ([xshift=16mm, yshift=-4mm]a3.south east);
 \begin{pgfonlayer}{background}
 \node[draw, fill=background, rounded corners, fit=(nw2)(se2)] (add) {};
 \end{pgfonlayer}
@@ -273,69 +309,43 @@ Figure~\ref{fig:example_3AC} shows the 3AC that the CompCert frontend obtains fr
 
 \draw[exted] (m7.west) -- ++(-7mm,0) |- ([yshift=-1mm]a2.west);
 \draw[exted] (m4.west) -- ++(-9mm,0) |- ([yshift=1mm]a2.west);
-\draw[exted] ([yshift=-1mm]a3.east) -- ++(16mm,0) |- (m6.east);
-\draw[exted] ([yshift=1mm]a3.east) -- ++(18mm,0) |- (m3.east);
+\draw[exted] ([yshift=-1mm]a3.east) -- ++(19mm,0) |- (m6.east);
+\draw[exted] ([yshift=1mm]a3.east) -- ++(21mm,0) |- (m3.east);
 
 \end{tikzpicture}
-\caption{Two FSMDs. A few points to make: (1) the dotted lines don't mean anything, and are just indicative of how control moves between the state machines, (2) meaning of the asterisk.}
-\label{fig:fsmds}
+\caption{Running example: HTL representation comprising two state machines}
+\label{fig:example_HTL}
 \end{figure}
 
+Execution begins in state 9 of the \lstinline{main} machine, and proceeds through successive states until it reaches state 7, in which the \lstinline{add} machine's \lstinline{rst} signal is raised. This puts the \lstinline{add} machine into state 2. When the \lstinline{main} machine advances to state 12, that \lstinline{rst} signal is lowered; the \lstinline{add} machine then begins its computation while the \lstinline{main} machine spins in state 12. When the \lstinline{add} machine has finished its computation (state 1), it asserts its \lstinline{fin} signal. This allows the \lstinline{main} machine to progress from state 12. Finally, the \lstinline{add} machine lowers its \lstinline{fin} and waits in state 3 until the next call.
 
+The same sequence of events can also be understood using a timing diagram, as given in Figure~\ref{fig:timingdiagram}. In that diagram, the red lines indicate unspecified values. We see that each call of \lstinline{add} begins with a pulse on \lstinline{add.rst} (fifth waveform) and ends with a pulse on \lstinline{add.fin} (sixth waveform).
 
 \begin{figure}
-\begin{tikzpicture}[yscale=-1]
-\node(fun1) at (1.5,2) {function};
-\node(fun2) at (0,2) {function};
-\node[anchor=west](C) at (-2,2) {\bf C:};
-\node(CFG1) at (1.5,3) {CFG};
-\node(CFG2) at (0,3) {CFG};
-\node(CFG) at (0.75,4) {CFG};
-\node[anchor=west](TAC) at (-2,3) {\bf 3AC:};
-\node(FSMD) at (0.75,5) {FSMD};
-\node[anchor=west](HTL) at (-2,5) {\bf HTL:};
-\node(module) at (0.75,6) {module};
-\node[anchor=west](Verilog) at (-2,6) {\bf Verilog:};
-\draw[->] (fun1) to node [auto] {CompCert frontend} (CFG1);
-\draw[->] (fun2) to (CFG2);
-\draw[->] (CFG1) to node [auto, pos=0.2] {inlining} (CFG);
-\draw[->] (CFG2) to (CFG);
-\draw[->] (CFG) to node [auto] {FSMD generation} (FSMD);
-\draw[->] (FSMD) to node [auto] {Verilog generation} (module);
-\end{tikzpicture}
-\caption{Key compilation passes and intermediate languages in Vericert~\cite{vericert}}
-\label{fig:vericert_flow}
-
-\begin{tikzpicture}[yscale=-1]
-\node(fun1) at (1.5,2) {function};
-\node(fun2) at (0,2) {function};
-\node[anchor=west](C) at (-2,2) {\bf C:};
-\node(CFG1) at (1.5,3) {CFG};
-\node(CFG2) at (0,3) {CFG};
-\node[anchor=west](TAC) at (-2,3) {\bf 3AC:};
-\node(FSMD1) at (1.5,4) {FSMDE};
-\node(FSMD2) at (0,4) {FSMDE};
-\node(FSMD3) at (1.5,5) {FSMDE};
-\node(FSMD4) at (0,5) {FSMDE};
-\node[anchor=west](HTL) at (-2,4) {\bf HTL:};
-\node(module) at (0.75,6) {module};
-\node[anchor=west](Verilog) at (-2,6) {\bf Verilog:};
-\draw[->] (fun1) to node [auto] {CompCert frontend} (CFG1);
-\draw[->] (fun2) to (CFG2);
-\draw[->] (CFG1) to node [auto] {FSMDE generation} (FSMD1);
-\draw[->] (CFG2) to (FSMD2);
-\draw[->, dashed] (FSMD1) to node [auto] {renaming} (FSMD3);
-\draw[->, dashed] (FSMD2) to (FSMD4);
-\draw[->, dashed] (FSMD3) to node [auto, pos=0.2] {Verilog generation} (module);
-\draw[->, dashed] (FSMD4) to (module);
-\end{tikzpicture}
-\caption{Key compilation passes and intermediate languages in Vericert-Fun, with dashed arrows indicating passes that have been implemented but not verified}
-\label{fig:vericert-fun_flow}
+\begin{tikztimingtable}[timing/d/background/.style={fill=white}, timing/xunit=1em]
+{\tt\small clk} & 0.5L 38{0.5C} \\
+{\tt\small rst} & 0.5H 19L \\
+{\tt\small fin} & 0.5X 17L H L \\
+{\tt\small state} & 0.5X D{9} D{8} D{7} 4D{12} D{6} D{5} D{4} 4D{10} D{3} D{2} D{1} 2D{11} \\
+{\tt\small rst} & 3.5X H 6L H 8L \\
+{\tt\small fin} & 4.5X 2L H 6L H 5L \\
+{\tt\small state} & 4.5X D{2} D{1} 5D{3} D{2} D{1} 6D{3} \\
+\extracode
+\foreach\i in {1,2,...,19}
+\node[help lines, anchor=west, inner sep=0] at (\i-0.5,2.25) {\tiny \i};
+\begin{pgfonlayer}{background}
+  \vertlines[help lines]{0.5,1.5,...,18.5}
+\end{pgfonlayer}
+\draw[decoration={brace,mirror,raise=5pt},decorate] (-3,-1) to node[left=6pt] {\tt\small main} (-3,-6.5);
+\draw[decoration={brace,mirror,raise=5pt},decorate] (-3,-7) to node[left=6pt] {\tt\small add} (-3,-12.5);
+\end{tikztimingtable}
+\caption{Timing diagram for the state machines in Figure~\ref{fig:example_HTL}}
+\label{fig:timingdiagram}
 \end{figure}
 
 
-
-A few points that we might want to answer at some point:
+\section{Rough notes}
+A few points that we might want to address at some point:
 
 \begin{itemize}
 
@@ -354,19 +364,22 @@ A few points that we might want to answer at some point:
 
 \item What is needed for the correctness proof? (Semantics for C, semantics for Verilog, ...)
 
+\item We considered having multiple Verilog modules, which would be more idiomatic, but this would require more invasive changes to the semantics.
+
 \end{itemize}
 
 
 \appendix
 
-\begin{figure}
-% NB: reg_3 renamed to reg_7
+\section{Verilog output for running example}
+
 \begin{lstlisting}
 module main (clk, rst, ret, fin)
   input clk, rst;
   output reg [31:0] ret;
   output reg fin;
-  reg[31:0] state, reg_1, reg_2, reg_3, reg_4, reg_5, reg_6;
+  reg[31:0] state;
+  reg[31:0] reg_1, reg_2, reg_3, reg_4, reg_5, reg_6;
   reg add_rst, add_fin; 
   reg[31:0] add_ret, add_x2, add_x1, reg_7, add_state;
   
@@ -434,9 +447,6 @@ module main (clk, rst, ret, fin)
     endcase
 endmodule
 \end{lstlisting}
-\caption{Example Verilog code}
-\label{fig:example_Verilog}
-\end{figure}