Update on Overleaf.

1 files changed, 114 insertions, 8 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index e1f8f0d..0f7c879 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -3,6 +3,8 @@
 \usepackage[textsize=small,shadow]{todonotes}%
 \usepackage{soul}
 \usepackage{subcaption}
+\usepackage{tikz-timing}
+\usetikzlibrary{fit}
 
 \usepackage{listings}
 \lstset{
@@ -39,6 +41,7 @@ escapeinside=||,
 \COMMENTStrue
 \newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [\![#2:} #3{\bf ]\!]}}\fi}
 \newcommand\JW[2][]{\st{#1}\Comment{red!75!black}{JW}{#2}}
+\newcommand\YH[2][]{\st{#1}\Comment{blue!50!green}{YH}{#2}}
 
 
 \newcommand{\citeintext}[1] {\citeauthor{#1} in \citeyear{#1}~\cite{#1}}
@@ -105,9 +108,7 @@ Figure~\ref{fig:example_C} shows a simple C file that we shall employ as a worke
 
 \begin{figure}
 \begin{lstlisting}
-int add(int a, int b) {
-  |\HL0{return a + b;}|
-}
+int add(int a, int b) { |\HL0{return a + b;}| }
 
 int main() {
   |\HL1{int v = 0;}|
@@ -120,7 +121,7 @@ int main() {
 \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?}
+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}
 
 \begin{figure}
 \begin{lstlisting}
@@ -184,13 +185,13 @@ add (x2, x1) {
 \begin{lstlisting}
 main () {
   externctrl {
-    |\HL2{add\_0\_x2 -> add.param\_0;}|
-    |\HL2{add\_0\_x1 -> add.param\_1;}|
+    |\HL2{add\_0\_x2 -> add.param[0];}|
+    |\HL2{add\_0\_x1 -> add.param[1];}|
     |\HL2{add\_0\_fin -> add.fin;}|
     |\HL2{add\_0\_rst -> add.rst;}|
     |\HL2{add\_0\_ret -> add.ret;}|
-    |\HL3{add\_1\_x2 -> add.param\_0;}|
-    |\HL3{add\_1\_x1 -> add.param\_1;}|
+    |\HL3{add\_1\_x2 -> add.param[0];}|
+    |\HL3{add\_1\_x1 -> add.param[1];}|
     |\HL3{add\_1\_fin -> add.fin;}|
     |\HL3{add\_1\_rst -> add.rst;}|
     |\HL3{add\_1\_ret -> add.ret;}|
@@ -238,6 +239,111 @@ main () {
 \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}
+
+\definecolor{background}{HTML}{eeeeee}
+\begin{figure}
+\centering
+\tikzset{
+st/.style={draw=black, fill=white, rounded corners, align=left, font=\tt\footnotesize, 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},
+node distance=5mm
+}
+\begin{tikzpicture}
+\node[st] (m9) at (0,0) {reg\_3 <= 0;};
+\node[st, below=of m9] (m8) {reg\_6 <= 1;};
+\node[st, below=of m8] (m7) {add.rst <= 1; \\ add.param\_0 <= reg\_3; \\ add.param\_1 <= reg\_6;};
+\node[st, below=of m7] (m12) {add.rst <= 0; \\ reg\_1 <= add.ret;};
+\node[st, below=of m12] (m6) {reg\_3 <= reg\_1;};
+\node[st, below=of m6] (m5) {reg\_5 <= 2;};
+\node[st, below=of m5] (m4) {add.rst <= 1; \\ add.param\_0 <= reg\_3; \\ add.param\_1 <= reg\_5;};
+\node[st, below=of m4] (m10) {add.rst <= 0; \\ reg\_2 <= add.ret;};
+\node[st, below=of m10] (m3) {reg\_3 <= reg\_2;};
+\node[st, below=of m3] (m2) {reg\_4 <= reg\_3;};
+\node[st, below=of m2] (m1) {fin = 1; \\ ret = reg\_4;};
+\node[st, below=of m1] (m11) {fin <= 0;};
+
+\node[st, below=2cm of m11] (a2) {reg\_7 <= \{\{x2 + x1\} + 0\};};
+\node[st, below=of a2] (a1) {fin = 1; \\ ret = reg\_7;};
+\node[st, below=of a1] (a3) {fin <= 0;};
+
+\draw[ed] (m9) to node[edlab] {!rst} (m8);
+\draw[ed] (m8) to node[edlab] {!rst} (m7);
+\draw[ed] (m7) to node[edlab] {!rst} (m12);
+\draw[ed] (m12) to node[edlab] {!rst \&\& add.fin} (m6);
+\draw[ed] (m6) to node[edlab] {!rst} (m5);
+\draw[ed] (m5) to node[edlab] {!rst} (m4);
+\draw[ed] (m4) to node[edlab] {!rst} (m10);
+\draw[ed] (m10) to node[edlab] {!rst \&\& add.fin} (m3);
+\draw[ed] (m3) to node[edlab] {!rst} (m2);
+\draw[ed] (m2) to node[edlab] {!rst} (m1);
+\draw[ed] (m1) to node[edlab] {!rst} (m11);
+\draw[ed] (m12) to[loop right, looseness=2, out=-4, in=4] node[edlab, swap] {!rst \&\& \\ !add.fin} (m12);
+\draw[ed] (m10) to[loop right, looseness=2, out=-4, in=4] node[edlab, swap] {!rst \&\& \\ !add.fin} (m10);
+\draw[ed] (m11) to[loop below, looseness=10, pos=0.15] node[edlab] {!rst} (m11);
+
+\node[inner sep=1pt] (ast1) at ([xshift=5mm, yshift=-5mm]m9.south east) {*};
+\draw[ed] (ast1.north) to[bend right] node[edlab, swap] {rst} (m9.east);
+
+\draw[ed] (a2) to node[edlab] {!rst} (a1);
+\draw[ed] (a1) to node[edlab] {!rst} (a3);
+\draw[ed] (a3) to[loop below, looseness=10, pos=0.15] node[edlab] {!rst} (a3);
+
+\node[inner sep=1pt] (ast2) at ([xshift=5mm, yshift=-5mm]a2.south east) {*};
+\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);
+\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);
+\begin{pgfonlayer}{background}
+\node[draw, fill=background, rounded corners, fit=(nw2)(se2)] (add) {};
+\end{pgfonlayer}
+\node[tit, above=2mm of a2] (labadd) {\bfseries add(x2,x1)};
+
+\foreach\i in {1,2,...,12}
+  \node[lab] at (m\i.north west) {\i};
+\foreach\i in {1,2,3}
+  \node[lab] at (a\i.north west) {\i};
+  
+
+
+\draw[exted] (m7.west) -- ++(-9mm,0) |- ([yshift=-1mm]a2.west);
+\draw[exted] (m4.west) -- ++(-7mm,0) |- ([yshift=1mm]a2.west);
+\draw[exted] ([yshift=-1mm]a3.east) -- ++(18mm,0) |- (m6.east);
+\draw[exted] ([yshift=1mm]a3.east) -- ++(16mm,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}
+\end{figure}
+
+\begin{figure}
 % NB: reg_3 renamed to reg_7
 \begin{lstlisting}
 module main (clk, rst, ret, fin) {