Fix some things

1 files changed, 4 insertions, 6 deletions

diff --git a/main.tex b/main.tex
index 5f191f1..2e03ff0 100644
--- a/main.tex
+++ b/main.tex
@@ -94,9 +94,7 @@
 \email{j.wickerson@imperial.ac.uk}
 
 \begin{abstract}
-  With hardware designs becoming ever more complex\JW{,} and demand for custom accelerators ever growing, high-level synthesis (HLS) is increasingly being relied upon.  However, HLS is known to be quite flaky, with each tool supporting subtly different fragments of the input language and sometimes even generating incorrect designs. \JW{Probably no paragraph break needed here.}
-
-  We argue that a formally verified HLS tool could solve this issue by dramatically reducing the amount of trusted code, and providing a formal description of the input language that is supported. To this end, we have developed \JW{are developing?} \vericert{}, a formally verified HLS tool, based on \compcert{}, a formally verified C compiler.
+  With hardware designs becoming ever more complex, and demand for custom accelerators ever growing, high-level synthesis (HLS) is increasingly being relied upon.  However, HLS is known to be quite flaky, with each tool supporting subtly different fragments of the input language and sometimes even generating incorrect designs.  We argue that a formally verified HLS tool could solve this issue by dramatically reducing the amount of trusted code, and providing a formal description of the input language that is supported. To this end, we are developing \vericert{}, a formally verified HLS tool, based on \compcert{}, a formally verified C compiler.
 \end{abstract}
 
 \maketitle
@@ -112,15 +110,15 @@
 
 Research in high-level synthesis (HLS) often concentrates on performance: trying to achieve the lowest area with the shortest run-time.  What is often overlooked is ensuring that the HLS tool is correct, which means that it outputs hardware designs that are equivalent to the behavioural input.
 
-When working with HLS tools, it is often assumed that they transform the behavioural input into a semantically equivalent design~\cite{lahti19_are_we_there_yet} for example. \JW{Not sure how to parse the `for example' part there.}  However, this is not the case, and as with all complex pieces of software there are bugs in HLS tools as well.  For example, Vivado HLS was found to incorrectly apply pipelining optimisations\footnote{\url{https://bit.ly/vivado-hls-pipeline-bug}} or generate incorrect designs silently when straying outside \JWcouldcut{of} the supported \JW{fragment of} C.\footnote{\url{https://bit.ly/vivado-hls-pointer-bug}}  These types of bugs are difficult to identify, and exist because \JWcouldcut{firstly} it is not quite clear \JW{firstly} what input these tools support, and secondly whether the output design actually behaves the same as the input.
+When working with HLS tools, it is often assumed that they transform the behavioural input into a semantically equivalent design~\cite{lahti19_are_we_there_yet}.  However, this is not the case, and as with all complex pieces of software there are bugs in HLS tools as well.  For example, Vivado HLS was found to incorrectly apply pipelining optimisations\footnote{\url{https://bit.ly/vivado-hls-pipeline-bug}} or generate incorrect designs silently when straying outside the supported fragment of C.\footnote{\url{https://bit.ly/vivado-hls-pointer-bug}}  These types of bugs are difficult to identify, and exist because it is not quite clear firstly what input these tools support, and secondly whether the output design actually behaves the same as the input.
 
-\paragraph{\bf Our position:} We believe that a formally verified \JWreplace{high-level synthesis}{HLS} tool could be the solution to these problems.  It not only guarantees that the output is correct, but also brings a formal specification of the input and output language semantics.  These are the only parts of the compiler that need to be trusted, and if these are well-specified, then the behaviour of the resulting design can be fully trusted.  In addition to that, if the semantics of the input language are taken from a tool that is widely trusted already, then there should not be any strange behaviour; the resultant design will either behave exactly like the input specification, or the translation will fail early at compile time.  To this end, we \JWreplace{have built}{are building} a formally verified HLS tool called \vericert{}~\cite{herklotz21_formal_verif_high_level_synth}.
+\paragraph{\bf Our position:} We believe that a formally verified HLS tool could be the solution to these problems.  It not only guarantees that the output is correct, but also brings a formal specification of the input and output language semantics.  These are the only parts of the compiler that need to be trusted, and if these are well-specified, then the behaviour of the resulting design can be fully trusted.  In addition to that, if the semantics of the input language are taken from a tool that is widely trusted already, then there should not be any strange behaviour; the resultant design will either behave exactly like the input specification, or the translation will fail early at compile time.  To this end, we are building a formally verified HLS tool called \vericert{}~\cite{herklotz21_formal_verif_high_level_synth}.
 
 In what follows, we will argue our position by presenting several possible \emph{objections} to our position, and then responding to each in turn.
 
 \section{Arguments against formalised HLS}
 
-\objection{People should not be designing hardware in C to begin with}{Formally verifying HLS of C is the wrong approach.  C should not be used to design hardware, let alone hardware where reliability is crucial.  First of all, HLS tools are not unreliable in terms of correctness, but more so in terms \JW{of} the quality of the hardware\JW{,} which can be quite unpredictable~\cite{nigam20_predic_accel_desig_time_sensit_affin_types}.  For example, \JW{when} writing C for an HLS tool, small changes in the input could result in large differences in area and performance \JWreplace{for}{of} the resulting hardware, \JWcouldcut{leading to a kind of flakiness in the output}.  \JWreplace{Instead}{On the other hand}, there have been many efforts to formally verify the translation of high-level hardware description languages like Bluespec with K\^{o}i\-ka~\cite{bourgeat20_essen_blues}, \JWreplace{formalising}{to formalise} the synthesis of Verilog into technology-mapped net-lists with Lutsig~\cite{loow21_lutsig}, or \JWreplace{formalising}{to formalise} circuit design in Coq itself to ease design verification~\cite{choi17_kami,singh_silver_oak}.}
+\objection{People should not be designing hardware in C to begin with}{Formally verifying HLS of C is the wrong approach.  C should not be used to design hardware, let alone hardware where reliability is crucial.  First of all, HLS tools are not unreliable in terms of correctness, but more so in terms of the quality of the hardware, which can be quite unpredictable~\cite{nigam20_predic_accel_desig_time_sensit_affin_types}.  For example, when writing C for an HLS tool, small changes in the input could result in large differences in area and performance \JWreplace{for}{of} the resulting hardware, \JWcouldcut{leading to a kind of flakiness in the output}.  \JWreplace{Instead}{On the other hand}, there have been many efforts to formally verify the translation of high-level hardware description languages like Bluespec with K\^{o}i\-ka~\cite{bourgeat20_essen_blues}, \JWreplace{formalising}{to formalise} the synthesis of Verilog into technology-mapped net-lists with Lutsig~\cite{loow21_lutsig}, or \JWreplace{formalising}{to formalise} circuit design in Coq itself to ease design verification~\cite{choi17_kami,singh_silver_oak}.}
 
 \response{} Verifying HLS is also important.  First, C is often the starting point for hardware designs, as initial models are written in those languages to get a quick prototype~\cite{gajski10_what_hls}, so it is only natural to continue using C when designing the hardware.  Not only is HLS from C becoming more popular, but much of that convenience comes from the easy behavioural testing that HLS allows to ensure correct functionality of the design~\cite{lahti19_are_we_there_yet}.  This assumes that HLS tools are correct.  Finally, even though unpredictability of the output of HLS tools might seem like the largest issue, working on a functionally correct HLS tool provides a good baseline to work on improving the predictability of the output as well.  Reasoning about correctness could maybe be extended with proofs about the variability of the generated output hardware, thereby also improving the quality of the output.  \JW{In this vein, }\compcert{}~\cite{leroy09_formal_verif_realis_compil}, an existing formally verified C compiler, has recently been extended with a proof of preservation of constant-time~\cite{barthe20_formal_c}, and a similar approach could be taken to \JWcouldcut{improve} to prove properties about the preservation of the hardware area or performance. % JW: Yes, this is great stuff.