various

1 files changed, 18 insertions, 10 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index ecb0a4c..9b799b4 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -183,9 +183,7 @@ tit/.style={anchor=north west, font=\tt},
 edlab/.style={auto, inner sep=2pt, align=left, font=\tt}
 }
 
-In this section, we shall explain the implementation of Vericert-Fun with the aid of the worked example shown in Figure~\ref{fig:example_C}. The basic idea is shown at the bottom of Figure~\ref{fig:flow}. \JW{Add more text here to explain the rough idea of Vericert-Fun.}
-
-We shall use the small C program in Figure~\ref{fig:example_C} as a worked example. Note that each instruction is colour-coded so it can be tracked through the compilation stages.
+In this section, we shall explain the implementation of Vericert-Fun, using Figure~\ref{fig:example_C} as a worked example. The basic idea is shown at the bottom of Figure~\ref{fig:flow}: we avoid inlining the function calls at the 3AC level (except in certain circumstances described below), instead maintaining one state machine per function. All the state machines run simultaneously, and function calls are implemented by sending messages between the state machines. We combine all of these state machines into a single Verilog module, after renaming variables as necessary to avoid clashes.
 
 \begin{figure}
 \centering
@@ -201,7 +199,7 @@ int main() {
   |\HL4{return v;}|
 }
 \end{lstlisting}
-\caption{Running example: C program}
+\caption{Running example: C program, with each instruction colour-coded so it can be tracked through the compilation stages}
 \label{fig:example_C}
 \end{figure}
 
@@ -365,8 +363,24 @@ The same sequence of events can also be understood using a timing diagram, as gi
 \label{fig:timingdiagram}
 \end{figure}
 
+\JW{Still need to talk about:
+\begin{itemize}
+\item the additional idle state at the end
+\item externctrl
+\item alternative implementations that we considered, e.g. separate Verilog modules
+\end{itemize}}
+
+\section{Performance evaluation}
+
+\JW{Todo.}
+
+
 \section{Proving Vericert-Fun correct}
 
+\JW{Todo:
+\begin{itemize}
+\item What is needed for the correctness proof? (Semantics for C, semantics for Verilog, ...)
+\end{itemize}}
 
 \section{Rough notes}
 A few points that we might want to address at some point:
@@ -384,12 +398,6 @@ A few points that we might want to address at some point:
 \item the execution on the FPGA could go wrong, e.g. as a result of cosmic rays.
 \end{itemize}
 
-\item What does Vericert currently do?
-
-\item What is needed for the correctness proof? (Semantics for C, semantics for Verilog, ...)
-
-\item We considered having multiple Verilog modules; this would be more idiomatic, but this would require more invasive changes to the semantics.
-
 \end{itemize}