Update on Overleaf.

2 files changed, 16 insertions, 12 deletions

diff --git a/conclusion.tex b/conclusion.tex
index b7daf71..a967e59 100644
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -16,10 +16,14 @@ Beyond this, we plan to implement scheduling and loop pipelining, since this all
 % JW: I chopped the following because we mentioned Six et al already.
 %recent work by \citet{six+20} indicates how these scheduling algorithms can be implemented in \compcert.
 %Another possibility is re-using registers, since \compcert{}'s 3AC does not include register allocation.
-Other optimisations include resource sharing to reduce the circuit area, and using tailored hardware operators that use hard IP blocks on chip and can be pipelined. 
+Other optimisations include resource sharing to reduce the circuit area, and using tailored hardware operators that exploit the hard IP blocks of the chip and can be pipelined. 
 % this could include multi-cycle operations and pipelining optimisations so that division and multiplication operators also become more efficient.
 
-Finally, it's worth considering how trustworthy \vericert{} is compared to other HLS tools. The guarantee of full functional equivalence between input and output that \vericert{} provides is a strong one, the semantics for the source and target languages are both well-established, and Coq is a mature and thoroughly tested system. However, \vericert{} cannot guarantee to provide an output for every valid input -- for instance, as remarked in Section~\ref{sec:proof:htl_verilog}, \vericert{} will error out if given a program with more than about four million instructions! -- but our evaluation indicates that it does not seem to error out too frequently. And of course, \vericert{} cannot guarantee that the final hardware produced will be correct, because the Verilog it generates must pass through a series of unverified tools along the way. That concern may be allayed in the future thanks to recent work by~\citet{10.1145/3437992.3439916} to produce a verified logic synthesis tool.
+Finally, it's worth considering how trustworthy \vericert{} is compared to other HLS tools. The guarantee of full functional equivalence between input and output has been both proven and fuzz-tested; the semantics for the source and target languages are both well established; and Coq is a mature and thoroughly tested system. Nonetheless, \vericert{} cannot guarantee to provide an output for every valid input -- for instance, as remarked in Section~\ref{sec:proof:htl_verilog}, \vericert{} will error out if given a program with more than about four million instructions! -- but our evaluation indicates that it does not seem to error out too frequently. And of course, \vericert{} cannot guarantee that the final hardware produced will be correct, because the Verilog it generates must pass through a series of unverified tools along the way. That concern may be allayed in the future thanks to recent work by~\citet{10.1145/3437992.3439916} to produce a verified logic synthesis tool.
+
+\subsection*{Acknowledgements}
+We'd like to thank Sandrine Blazy, Jianyi Cheng, Alastair Donaldson, and the anonymous reviewers for their helpful feedback. \JW{Might need adding to.}
+This work was financially supported by the EPSRC via the Research Institute for Verified Trustworthy Software Systems (VeTSS) and the IRIS Programme Grant (EP/R006865/1).
 
 
 %%% Local Variables:
diff --git a/limitations.tex b/limitations.tex
index b218c11..9ed65ec 100644
--- a/limitations.tex
+++ b/limitations.tex
@@ -1,19 +1,19 @@
 \section{Limitations and Future Work}
 
-There are various limitations in \vericert{} compared to other HLS tools due to the fact that our main focus was on formally verifying the translation from 3AC to Verilog. In this section, we outline the current limitations of our tool and suggest how they can be overcome in future work, first describing limitations to the generated hardware, and then describing the limitations of the software input that \vericert{} accepts.
+There are various limitations in \vericert{} compared to other HLS tools due to the fact that our main focus was on formally verifying the translation from 3AC to Verilog. In this section, we outline the current limitations of our tool and suggest how they can be overcome in future work, first describing limitations to the generated hardware, and then describing the limitations on the software input that \vericert{} accepts.
 
 %\NR{You have very different types of limitations. I wonder if grouped them into software and hardware limitations respectively might simplify this section. Just a suggestion.}
 
-\subsection{Limitations and improvements to the hardware}
+\subsection{Limitations to the generated hardware}
 
-This section describes the current limitations and possible improvements that could be done to the generated hardware.
+%This section describes the current limitations and possible improvements that could be made to the generated hardware.
 
 \paragraph{Lack of instruction-level parallelism}
 
 %\JW{I'm hesitant about this paragraph. Yes, we have to write something about how future-proof Vericert is, as this is required by the reviewers and promised in our list of changes. But I worry that if we place too much emphasis on how straightforward it will be to add scheduling, then we'll make it harder for ourselves to publish a paper about adding scheduling (``But you said in your OOPSLA 2021 paper that this was all straightforward'' etc.) In what follows, I've tried to strike a balance -- see what you think.}\YH{Yeah I think I like the paragraph and the balance in it, I think it still explains that existing passes should not have to change.  I think reviewer 2 wanted a detailed explanation of this, but I do agree that it should not be needed in this paper.}
 The main limitation of \vericert{} is that it does not perform instruction scheduling, which means that instructions cannot be gathered into the same state and executed in parallel. 
 %This limitation is present by design so that the focus could be made on the initial proof of correctness of the translation of instructions with a sequential schedule.
-However, each language in \vericert{} was designed with scheduling in mind, so that these should not have to change fundamentally when it is implemented in the future. 
+However, each language in \vericert{} was designed with scheduling in mind, so that these should not have to change fundamentally when that is implemented in the future. 
 For instance, our HTL language already allows arbitrary Verilog to appear in each state of the FSMD; currently, each state just contains a single Verilog assignment, but when scheduling is added, it will contain a list of assignments that can all be executed in parallel. We expect to follow the lead of \citet{tristan08_formal_verif_trans_valid} and \citet{six+20}, who have previously added scheduling support to CompCert in a VLIW context, by invoking an external (unverified) scheduling tool and then using translation validation to verify that each generated schedule is correct (as opposed to verifying the scheduling tool itself). 
 %The translation from 3ACPar to HTL would not change conceptually, except for the fact that multiple instructions can now be translated into the same state. 
 %This means that the proof of translation from 3AC to HTL can also be adapted with minimal changes to the top-level of the proofs. 
@@ -27,27 +27,27 @@ For instance, our HTL language already allows arbitrary Verilog to appear in eac
 
 \paragraph{Lack of pipelined division}
 Pipelined operators can execute different stages of an operation in parallel, and thus perform several long-running operations simultaneously while sharing the same hardware.
-The introduction of pipelined operators to \vericert{}, especially for division, would alleviate the slow clock speed observed in the \polybench{} benchmarks with divisions included (Fig.~\ref{fig:polybench-div}). In HTL, pipelined operations could be represented in a similar fashion to load and store instructions, by using wires to communicate with an abstract computation block modelled in HTL and later replaced by a hardware implementation.
+The introduction of pipelined operators to \vericert{}, especially for division, would alleviate the slow clock speed observed in the \polybench{} benchmarks when divisions were included (Fig.~\ref{fig:polybench-div}). In HTL, pipelined operations could be represented in a similar fashion to load and store instructions, by using wires to communicate with an abstract computation block modelled in HTL and later replaced by a hardware implementation.
 %\NR{Are you describing using IP blocks? If so, you can generalise it to any IP block rather than just division.}\YH{I think I prefer just focusing on pipelined division for now, as that's specifically the issue, so that people know we have a plan to resolve specifically that.}
 %JW I've chopped the following sentence because it felt like it was going into too much detail. 
 %However, 3ACPar would have to be modified to also describe such instructions so that these can be placed optimally using the external scheduling algorithm.
 
-\subsection{Limitations and improvements to the software input}
+\subsection{Limitations on the software input}
 
-This section describes the limitations and possible improvements to the software input accepted by \vericert{}.
+%This section describes the limitations and possible improvements to the software input accepted by \vericert{}.
 
 \paragraph{Limitations with I/O}
 
-\vericert{} is currently limited in terms of I/O because the main function cannot accept any arguments if the Clight program is to be well-formed. However, just like \compcert{}, \vericert{} can actually compile main functions that have arbitrary arguments and will handle the inputs appropriately. Still, the main correctness theorem in \compcert{} assumes that the main function does not have any arguments, so it may be possible that unexpected behaviour is introduced. Moreover, external function calls that produce traces have not been implemented yet, but once they have, they could enable the C program to read and write values on a bus that is shared with various other components in the hardware design.
+\vericert{} is currently limited in terms of I/O because the main function cannot accept any arguments if the Clight program is to be well-formed.\footnote{Technically, \vericert{} (and indeed, \compcert{}) can compile main functions that have arbitrary arguments and will handle those inputs appropriately, but the correctness theorem offers no guarantees about such programs.} Moreover, external function calls that produce traces have not been implemented yet, but once they have, they could enable the C program to read and write values on a bus that is shared with various other components in the hardware design.
 
 \paragraph{Lack of support for global variables}
-In \compcert{}, each global variable is stored in its own memory.  A generalisation of the stack translation into a RAM block could therefore be performed to translate global variables in the same manner.  This would require a slight generalisation of pointers so that they store provenance information to ensure that each pointer accesses the right RAM. It would also be necessary to generalise the RAM interface so that it decodes the provenance information and indexes the right array.
+In \compcert{}, each global variable is stored in its own memory.  A generalisation of our translation of the stack into a RAM block could therefore translate global variables in the same manner.  This would require a slight generalisation of pointers so that they store provenance information to ensure that each pointer accesses the right RAM. It would also be necessary to generalise the RAM interface so that it decodes the provenance information and indexes the correct array.
 %\NR{Curiously, is memory analysis in your to-do list?}\YH{Well kind of, would be nice, but probably not sophisticated analysis.}
 
 \paragraph{Other language restrictions}
 C and Verilog handle signedness quite differently. By default, all operators and registers in Verilog (and HTL) are unsigned, so to force an operation to handle the bits as signed, both operators have to be forced to be signed. Moreover, Verilog implicitly resizes expressions to the largest needed size by default, which can affect the result of the computation.  This feature is not supported by the Verilog semantics we adopted, so to match the semantics to the behaviour of the simulator and synthesis tool, braces are placed around all expressions to inhibit implicit resizing.  Instead, explicit resizing is used in the semantics, and operations can only be performed on two registers that have the same size.
 
-Furthermore, equality checks between \emph{unsigned} variables are actually not supported, because this requires supporting the comparison of pointers, which should only be performed between pointers with the same provenance.  In \vericert{} there is currently no way to determine the provenance of a pointer, and it therefore cannot model the semantics of unsigned comparison in \compcert{}. This is not a severe restriction in practice however, because, since dynamic allocation is not supported either, equality comparison of pointers is rarely needed, and equality comparison of integers can still be performed by casting them both to signed integers.
+Furthermore, equality checks between \emph{unsigned} variables are actually not supported, because this requires supporting the comparison of pointers, which should only be performed between pointers with the same provenance.  In \vericert{} there is currently no way to determine the provenance of a pointer, and it therefore cannot model the semantics of unsigned comparison in \compcert{}. This is not a severe restriction in practice however, because in the absence of dynamic allocation, equality comparison of pointers is rarely needed, and equality comparison of integers can still be performed by casting them both to signed integers.
 
 Finally, the \texttt{mulhs} and \texttt{mulhu} instructions, which fetch the upper bits of a 32-bit multiplication, are not translated by \vericert{}, because 64-bit numbers are not supported. These instructions are only generated to optimise divisions by a constant that is not a power of two, so turning off constant propagation will allow these programs to pass without error.