Update on Overleaf.

1 files changed, 15 insertions, 12 deletions

diff --git a/proof.tex b/proof.tex
index 4566619..b0962de 100644
--- a/proof.tex
+++ b/proof.tex
@@ -2,6 +2,20 @@
 
 Now that the Verilog semantics have been adapted to the CompCert model, we are in a position to formally prove the correctness of our C-to-Verilog compilation.  This section describes the main correctness theorem that was proven and the main ideas behind the proof. The full Coq proof is available in auxiliary material.
 
+\subsection{Main challenges in the proof}
+
+The proof of correctness of the Verilog back end is quite different from the usual proofs performed in CompCert, mainly because of the difference in Verilog semantics compared to the standard CompCert intermediate languages and because of the translation of the memory model.
+
+\begin{itemize}
+\item First, because the memory model in our Verilog semantics is finite and concrete, but the CompCert memory model is more abstract and infinite with additional bounds, the equivalence of both these models needs to be proven.  Moreover, our memory is word-addressed for efficiency reasons, whereas CompCert's memory is byte-addressed. \JW{This point has been made a couple of times already by now. I think it's ok to say it again briefly here, but I'd be tempted to acknowledge that it's repetitive by prepending it with something like ``As already mentioned in Section blah,'' }
+
+\item Second, the Verilog semantics operates quite differently to the usual intermediate languages in CompCert.  All the CompCert intermediate languages use a map from control-flow nodes to instructions.  An instruction can therefore be selected using an abstract program pointer. Meanwhile, in the Verilog semantics the whole design is executed at every clock cycle, because hardware is inherently parallel. The program pointer is part of the design as well, not just part of an abstract state. This makes the semantics of Verilog simpler, but comparing it to the semantics of 3AC becomes more challenging, as one has to map the abstract notion of the state to concrete values in registers.
+\end{itemize}
+
+Together, these differences mean that translating 3AC directly to Verilog is infeasible, as the differences in the semantics are too large.  Instead, a new intermediate language needs to be introduced, called HTL, which bridges the gap in the semantics between the two languages.  HTL still consists of maps, like many of the other CompCert languages, however, each state corresponds to a Verilog statement. \JW{This is good text, but the problem is that it reads like you're introducing HTL here for the first time. In fact, the reader has already encountered HTL in Section 2. So this needs acknowledging.}
+
+\subsection{Formulating the correctness theorem}
+
 The main correctness theorem is analogous to that stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil}: for all Clight source programs $C$, if the translation to the target Verilog code succeeds, and $C$ has safe observable behaviour $B$ when executed, then the target Verilog code will have the same behaviour $B$. Here, a `safe' execution is one that either converges or diverges, but does not ``go wrong''. If the program does admit some wrong behaviour (like undefined behaviour in C), the correctness theorem does not apply. A behaviour, then, is either a final state (in the case of convergence) or divergence. In \compcert{}, a behaviour is also associated with a trace of I/O events, but since external function calls are not supported in \vericert{}, this trace will always be empty. This correctness theorem is also appropriate for HLS \JW{Perhaps it would be worth first explaining why somebody might think this correctness theorem might \emph{not} be appropriate for HLS. At the moment, it feels like you're giving the answer without saying the question. Is it to do with the fact that hardware tends to run forever?}, as HLS is often used as a part of a larger hardware design that is connected together using a hardware description language like Verilog.  This means that HLS designs are normally triggered multiple times and results are returned each time when the computation terminates, which is the property that the correctness theorem states.  Note that the compiler is allowed to fail and not produce any output; the correctness theorem only applies when the translation succeeds.
 
 %The following `backwards simulation' theorem describes the correctness theorem, where $\Downarrow$ stands for simulation and execution respectively.
@@ -16,20 +30,9 @@ The main correctness theorem is analogous to that stated in \compcert{}~\cite{le
 The theorem is a `backwards simulation' result (from target to source), following the terminology used in the \compcert{} literature~\cite{leroy09_formal_verif_realis_compil}. The theorem does not demand the `if' direction too, because compilers are permitted to resolve any non-determinism present in their source programs.
 In practice, Clight programs are all deterministic, as are the Verilog programs in the fragment we consider. This means that we can prove the correctness theorem above by first inverting it to become a forwards simulation result, following standard \compcert{} practice.
 
-Furthermore, to prove the forward simulation, it suffices to prove forward simulations between each intermediate language, as these results can be composed to prove the correctness of the whole HLS tool. 
+Furthermore, to prove the forward simulation, it suffices to prove forward simulations between each pair of consecutive intermediate languages, as these results can be composed to prove the correctness of the whole HLS tool. 
 The forward simulation from 3AC to HTL is stated in Lemma~\ref{lemma:htl} (Section~\ref{sec:proof:3ac_htl}), the forward simulation for the RAM insertion is shown in Lemma~\ref{lemma:htl_ram} (Section~\ref{sec:proof:ram_insertion}), then the forward simulation between HTL and Verilog is shown in Lemma~\ref{lemma:verilog} (Section~\ref{sec:proof:htl_verilog}) and finally, the proof that Verilog is deterministic is given in Lemma~\ref{lemma:deterministic} (Section~\ref{sec:proof:deterministic}).
 
-\subsection{Main challenges in the proof}
-
-The proof of correctness of the Verilog back end is quite different to the usual proofs performed in CompCert, mainly because of the difference in Verilog semantics compared to the standard CompCert intermediate languages and because of the translation of the memory model.
-
-First, because the memory model in our Verilog semantics is finite and concrete, but the CompCert memory model is more abstract and infinite with additional bounds, the equivalence of both these models needs to be proven.  Moreover, our memory is word-addressed for efficiency reasons, whereas CompCert's memory is byte-addressed.
-
-Second, the Verilog semantics operates quite differently to the usual intermediate languages in the backend.  All the CompCert intermediate languages use a map from control-flow nodes to instructions.  An instruction can therefore be selected using an abstract program pointer. On the other hand, in the Verilog semantics the whole design is executed at every clock cycle, because hardware is inherently parallel. The program pointer is part of the design as well, not just part of an abstract state.  This makes the semantics of Verilog simpler, but comparing it to the semantics of 3AC becomes more challenging, as one has to map the abstract notion of the state to concrete values in registers.
-
-Both these differences mean that translating 3AC directly to Verilog is infeasible, as the differences in the semantics is too large.  Instead, a new intermediate language needs to be introduced, called HTL, which bridges the gap in the semantics between the two languages.  HTL still consists of maps, like many of the other CompCert languages, however, each state corresponds to a Verilog statement.
-
-
 \subsection{Forward simulation from 3AC to HTL}\label{sec:proof:3ac_htl}
 
 As HTL is quite far removed from 3AC, this first translation is the most involved and therefore requires a larger proof, because the translation from 3AC instructions to Verilog statements needs to be proven correct in this step.  In addition to that, the semantics of HTL are also quite different to the 3AC semantics, as instead of defining small-step semantics for each construct in Verilog, the semantics are instead defined over one clock cycle and mirror the semantics defined for Verilog.  Lemma~\ref{lemma:htl} shows the result that needs to be proven in this subsection.