Update on Overleaf.

1 files changed, 13 insertions, 8 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index 43fc16e..e441688 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -103,22 +103,27 @@ This paper introduces \vericertfun: \vericert{} extended with function-level res
 \section{Introduction}
 \label{sec:introduction}
 
-The drive for faster, more energy-efficient computation has led to a surge in demand for custom hardware accelerators. This, in turn, has led to a great deal of interest in \emph{high-level synthesis} (HLS) as a means to program these devices.
-However, doubts have been raised about the reliability of the current crop of HLS tools. For instance, \citet{Herklotz2021_empiricalstudy} found numerous miscompilation bugs in commercial HLS tools including Xilinx Vivado HLS~\cite{xilinx_vitis}, the Intel HLS Compiler~\cite{intel_hls}, and LegUp~\cite{legup_CanisAndrew2011}. This unreliability can be a significant hindrance for developers, and it undermines the usefulness of HLS in safety- or security-critical settings. %It is therefore essential to ensure that HLS tools are as reliable as possible.
+The drive for faster, more energy-efficient computation has led to a surge in demand for custom hardware accelerators. This, in turn, has led to interest in \emph{high-level synthesis} (HLS) as a means to program these devices.
+Yet doubts have been raised about the reliability of the current crop of HLS tools. For instance, \citet{Herklotz2021_empiricalstudy} found numerous miscompilation bugs in Xilinx Vivado HLS~\cite{xilinx_vitis}, the Intel HLS Compiler~\cite{intel_hls}, and LegUp~\cite{legup_CanisAndrew2011}. This unreliability can be a significant hindrance for developers, and it undermines the usefulness of HLS in safety- or security-critical settings. %It is therefore essential to ensure that HLS tools are as reliable as possible.
 
 Aiming to address this issue is \vericert{}~\cite{vericert}, a new HLS tool whose correctness has been verified to the highest possible standard: a computer-checked proof that any Verilog design it produces will behave the same way as the C program given as input. %It is based on the CompCert~\cite{compcert_Leroy2009} verified C compiler.
-Clearly, however, it is not enough for an HLS tool simply to be \emph{correct}; the generated hardware must also enjoy high throughput, low latency, and good \emph{area efficiency} -- the last of which is the topic of this paper. A common optimisation employed by HLS tools to improve area efficiency is \emph{resource sharing}; that is, re-using hardware for more than one purpose. Accordingly, our work adds function-level resource sharing to \vericert{}, yielding a new prototype HLS tool called `\vericertfun'. In keeping with the aims of the \vericert{} project, work is ongoing to extend the correctness proof.
+Yet it is not enough for an HLS tool simply to be \emph{correct}; the generated hardware must also enjoy high throughput, low latency, and good \emph{area efficiency} -- the last of which is the topic of this paper. 
 
+A common optimisation employed by HLS tools to improve area efficiency is \emph{resource sharing}; that is, \JWchanged{mapping multiple operations to the same hardware unit}. Accordingly, our work adds function-level resource sharing to \vericert{}, yielding a new prototype HLS tool called `\vericertfun'. In line with the aims of the \vericert{} project, work is ongoing to extend the correctness proof.
 The entire \vericertfun{} development is fully open-source~\cite{vericertfun-github}, and more details about the implementation and proofs are available in a technical report~\cite{pardalos_thesis}.
 
 \section{Background}
 
-\paragraph{The Coq proof assistant} \vericert{} is implemented using Coq~\cite{coq}, which means it consists of a collection of functions that define the compilation process, together with the proof of a theorem stating that those definitions constitute a correct HLS tool. Coq mechanically checks this proof using a formal mathematical calculus, and then automatically translates the function definitions into OCaml code that can be compiled and executed. 
-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 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 Coq proof assistant} \vericert{} is implemented in Coq~\cite{coq}, which means it consists of a collection of functions that define the compiler, together with the proof of a theorem that those definitions constitute a correct HLS tool. Coq mechanically checks this proof using a formal mathematical calculus, then translates the function definitions into OCaml code that can be compiled and executed. 
+Developing software within a proof assistant like Coq is widely held to be the gold standard for correctness, and recent years have shown that substantial systems can be produced in this way, such as database systems~\cite{malecha+10}, web servers~\cite{chlipala15}, and OS kernels~\cite{gu+16}. Coq has also been deployed in hardware design, 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 in Coq. CompCert accepts most of the C99 language, and generally performs comparably to 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~\cite{csmith} has found hundreds of bugs in GCC and LLVM but none in (the verified parts of) CompCert is a testament to the reliability of this development approach. That said, we cannot guarantee that \vericertfun{} designs will never go wrong, because of fallibilities in components not covered by the theorem, such as the synthesis toolchain~\cite{verismith} and the FPGA itself.
+\paragraph{The CompCert verified C compiler} Among the most celebrated applications of Coq is CompCert~\cite{compcert}, a lightly optimising C compiler with backend support for the Arm, x86, PowerPC, and Kalray VLIW architectures~\cite{six+20}. 
+% CompCert accepts most of the C99 language, and generally performs comparably to 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 those passes. 
+That the Csmith compiler testing tool~\cite{csmith} has found hundreds of bugs in GCC and LLVM but none in (the verified parts of) CompCert is a testament to the reliability of this development approach. 
+That said, we cannot guarantee \vericertfun{} designs will never go wrong, because of fallible components not covered by the theorem, such as the synthesis toolchain~\cite{verismith} and the FPGA itself.
  
 \paragraph{The \vericert{} verified HLS tool}