Update on Overleaf.

1 files changed, 7 insertions, 7 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index c0650ce..1f39e0f 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -112,16 +112,16 @@ The entire \vericertfun{} development is fully open-source~\cite{vericertfun-git
 
 Engineering a software system within a proof assistant like Coq is widely held to be the gold standard for correctness. Recent years have shown that it is feasible to design substantial pieces of software in this way, such as database management systems~\cite{malecha+10}, web servers~\cite{chlipala15}, and operating system kernels~\cite{gu+16}. Coq has also been successfully deployed in the hardware design process, both in academia~\cite{braibant+13, bourgeat+20} and in industry~\cite{silveroak}. It has even been applied specifically to HLS: Faissole et al.~\cite{faissole+19} used it to verify that HLS optimisations respect dependencies in the source code.
 
-\paragraph{The CompCert verified C compiler} Among the most celebrated applications of Coq is the CompCert project~\cite{compcert}. CompCert is a lightly optimising C compiler, with backend support for the Arm, x86, PowerPC, and Kalray VLIW architectures~\cite{six+20}, that has been implemented and proven correct using Coq. CompCert accepts most of the C99 language, and generally produces code of comparable performance to that produced by GCC at optimisation level \texttt{-O1}. It transforms its input through a series of ten intermediate languages before generating the final output. This design ensures that each individual pass remains relatively simple and hence feasible to prove correct. The correctness proof of the entire compiler is formed by composing the correctness proofs of each of its passes. 
+\paragraph{The CompCert verified C compiler} Among the most celebrated applications of Coq is the CompCert project~\cite{compcert}. CompCert is a lightly optimising C compiler, with backend support for the Arm, x86, PowerPC, and Kalray VLIW architectures~\cite{six+20}, that has been implemented and proven correct in Coq. CompCert accepts most of the C99 language, and generally produces code of comparable performance to that produced by GCC at \texttt{-O1}. It transforms its input through a series of ten intermediate languages before generating the final output. This design ensures that each individual pass remains relatively simple and hence feasible to prove correct. The correctness proof of the entire compiler is formed by composing the correctness proofs of each of its passes. 
 
-That the Csmith compiler testing tool has found hundreds of bugs in GCC and LLVM but has never found a single bug in (the verified parts of) CompCert~\cite{csmith} is a testament to the reliability of this development approach. That said, we cannot guarantee that hardware produced via \vericertfun{} will never go wrong, because of fallibilities in components not covered by the correctness theorem, including the computer checking the proofs, the pretty-printer of the final Verilog design, the synthesis toolchain~\cite{verismith}, and the FPGA device itself.
+That the Csmith compiler testing tool has found hundreds of bugs in GCC and LLVM but none in (the verified parts of) CompCert~\cite{csmith} is a testament to the reliability of this development approach. That said, we cannot guarantee that hardware produced via \vericertfun{} will never go wrong, because of fallibilities in components not covered by the theorem, including the computer checking the proofs, the synthesis toolchain~\cite{verismith}, and the FPGA device itself.
  
 \paragraph{The \vericert{} verified HLS tool}
 
-Introduced by \citet{vericert}, \vericert{} is a verified C-to-Verilog HLS tool. It is an extension of CompCert, essentially augmenting the existing verified C compiler with a new hardware-oriented intermediate language (called HTL) and a Verilog backend. In its current form, \vericert{} performs no significant optimisations beyond those it inherits from CompCert's frontend. This results in performance generally about one order of magnitude slower than that achieved by comparable, unverified HLS tools such as LegUp~\cite{legup_CanisAndrew2011}.
-
-\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').
+Introduced by \citet{vericert}, \vericert{} is a verified C-to-Verilog HLS tool. It was built by extending CompCert with a new hardware-oriented intermediate language (called HTL) and a Verilog backend. \vericert{} currently performs no significant optimisations beyond those inherited from CompCert's frontend. This results in performance generally about one order of magnitude slower than that achieved by comparable, unverified HLS tools.
 
+\vericert{} branches off from CompCert at the intermediate language called \emph{register-transfer language} (RTL). \JW{Got up to here; will finish word-chopping pass tomorrow morning.} 
+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 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 \emph{finite state machine with datapath} (FSMD). 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.
 
 The overall \vericert{} flow is shown at the top of Figure~\ref{fig:flow}. The key point to note here is the `inlining' step, which folds all function definitions into their call sites. This allows \vericert{} to make the simplifying assumption that there is only a single CFG, but has the unwanted effect of duplicating hardware. In this work, we remove some of this inlining and hence some of the duplication.
@@ -445,7 +445,7 @@ We used the Icarus Verilog simulator to determine the cycle counts of the genera
 %introduces an extra state per function call. The impact on fmax is similarly minimal, ranging
 %between a 1.5\% increase and a 3.1\% decrease (0.2\% decrease on average).
 
-Figure~\ref{fig:results} compares the hardware generated by \vericertfun{} with that generated by \vericert{}, using the open-source (but unverified) \bambu{} HLS tool~\cite{pilato13_bambu} as a baseline. The top graph compares the area usage. We observe a consistent and substantial reduction in area usage across the benchmark programs, with \vericert{} consistently using more area than Bambu (1.4$\times$ on average) and \vericertfun{} almost always using less (0.7$\times$ on average). As expected, the benchmarks with the most function calls, such as \YH{name of benchmark?} and \YH{name of benchmark?} enjoy the biggest area savings. \JW{Revisit this text with the final experimental numbers.}
+Figure~\ref{fig:results} compares the hardware generated by \vericertfun{} with that generated by \vericert{}, using the open-source (but unverified) \bambu{} HLS tool~\cite{pilato13_bambu} as a baseline. The top graph compares the area usage. We observe a consistent and substantial reduction in area usage across the benchmark programs, with \vericert{} consistently using more area than Bambu (1.5$\times$ on average) and \vericertfun{} being much closer to Bambu (1.2$\times$ on average). As expected, the benchmarks with the most function calls, such as mvt and \YH{name of benchmark?} enjoy the biggest area savings. \JW{Revisit this text with the final experimental numbers.}
 
 The bottom graph compares the execution time. We observe that \vericertfun{} generates hardware that is almost exactly as fast as \vericert{}'s, with \vericertfun{} hardware being only 1\% slower on average. This can be attributed to the latency overhead of performing a function call. Hardware from \vericert{} and \vericertfun{} is significantly slower than \bambu's, which can be attributed to \vericert{} employing far fewer optimisations than the unverified \bambu{} tool.
 
@@ -471,7 +471,7 @@ The bottom graph compares the execution time. We observe that \vericertfun{} gen
       ymode=log,
       ybar=0.4pt,
       width=0.6\textwidth,
-      height=0.32\textwidth,
+      height=0.25\textwidth,
       /pgf/bar width=2pt,
       legend pos=north east,
       log ticks with fixed point,