Update on Overleaf.

1 files changed, 7 insertions, 8 deletions

diff --git a/method.tex b/method.tex
index 8841208..a06b2a0 100644
--- a/method.tex
+++ b/method.tex
@@ -78,13 +78,13 @@ This section describes how test-cases are generated (\S\ref{sec:method:csmith}),
     \end{tabular}
 \end{table}
 
-Csmith exposes several parameters through which the user can adjust how often various C constructs appear in the randomly generated programs. Table~\ref{tab:properties} describes how we configured these parameters.
+Csmith exposes several parameters through which the user can adjust how often various C constructs appear in the randomly generated programs. Table~\ref{tab:properties} describes how we configure these parameters.
 %\paragraph{Significant probability changes}
 %Table~\ref{tab:properties} lists the main changes that we put in place to ensure that HLS tools are able to synthesise all of our generated programs. 
-Our overarching aim is to make the programs tricky for the tools to handle correctly (in order to maximise our chances of exposing bugs), while keeping the synthesis and simulation times low (in order to maximise the rate at which tests can be run).
+Our overarching aim is to make the programs tricky for the tools to handle correctly (to maximise our chance of exposing bugs), while keeping the synthesis and simulation times low (to maximise the rate at which tests can be run).
 For instance, we increase the probability of generating \code{if} statements so as to increase the number of control paths, but we reduce the probability of generating \code{for} loops and array operations since they generally increase run times but not hardware complexity.
 We disable various features that are not supported by HLS tools such as assignments inside expressions, pointers, and union types.
-We avoid floating-point numbers since they typically involve external libraries or use of hard IPs on FPGAs, which make it hard to reduce bugs to a minimal form.
+We avoid floating-point numbers since they typically involve external libraries or hard IPs on FPGAs, which make it hard to reduce bugs to a minimal form.
 %Relatedly, we reduce the probability of generating \code{break}, \code{goto}, \code{continue} and \code{return} statements, because with fewer \code{for} loops being generated, these statements tend to lead to uninteresting programs that simply exit prematurely.
 
 %\paragraph{Important restrictions}
@@ -122,7 +122,7 @@ We avoid floating-point numbers since they typically involve external libraries
 
 To prepare the programs generated by Csmith for HLS testing, we modify them in two ways. First, we inject random HLS directives, which instruct the HLS tool to perform certain optimisations, including: loop pipelining, loop unrolling, loop flattening, loop merging, expression balancing, function pipelining, function-level loop merging, function inlining, array mapping, array partitioning, and array reshaping. Some directives can be applied via a separate configuration file (.tcl), some require us to add labels to the C program (e.g. to identify loops), and some require placing pragmas at particular locations in the C program.
 
-The second modification we make has to do with the top-level function. Each program generated by Csmith ends its execution by printing a hash of all its variables' values, in the hope that any miscompilations will be exposed through this hash value. We found that Csmith's built-in hash function led to infeasibly long synthesis times, so we replaced it with our own simple XOR-based one.
+The second modification has to do with the top-level function. Each program generated by Csmith ends its execution by printing a hash of all its variables' values, in the hope that any miscompilations will be exposed through this hash value. We found that Csmith's built-in hash function led to infeasibly long synthesis times, so we replace it with our own simple XOR-based one.
 
 Finally, we generate a synthesisable testbench that executes the main function of the original C program, and a tool-specific script that instructs the HLS tool to create a design project and then build and simulate the design.
 
@@ -179,10 +179,9 @@ Finally, we generate a synthesisable testbench that executes the main function o
 %Figure~\ref{fig:method:toolflow} shows the three stages of testing, depicted as the testing environment in the dashed area.
 For each HLS tool in turn, we compile the C program to RTL and then simulate the RTL. 
 We also compile the C program using GCC and execute it. 
-Although each HLS tool has its own built-in C compiler that could be used to obtain the reference output, we prefer to obtain the reference output ourselves in order to minimise our reliance on the tool that is being tested.
+Although each HLS tool has its own built-in C compiler that could be used to obtain the reference output, we prefer to obtain the reference output ourselves in order to minimise our reliance on the tool being tested.
 
-To ensure that our testing scales to a large number of large programs, we also enforce several time-outs: we set a 5-minute time-out for C execution and a 2-hour time-out for C-to-RTL synthesis and RTL simulation.
-We do not count time-outs as bugs, but we do record them.
+To ensure that our testing scales to a large number of large programs, we enforce several time-outs: we set a 5-minute time-out for C execution and a 2-hour time-out for C-to-RTL synthesis and RTL simulation. We do not count time-outs as bugs. %, but we do record them.
 
 %% JW: This paragraph is not really needed because we repeat the sentiment in the next subsection anyway.
 %There two types of bugs that we can encounter in this testing setup: programs that cause the HLS tool to crash during compilation (e.g. an unhandled assertion violation or a segmentation fault), and programs where the software execution and the RTL simulation do not return the same value. Programs that cause either type of error are given to the reduction stage, which aims to minimise the programs and (hopefully) identify the root cause(s).
@@ -213,7 +212,7 @@ Once we discover a program that crashes the HLS tool or whose C/RTL simulations
 %\creduce{} is an existing reducer for C and C++ and runs the reduction steps in parallel to converge as quickly as possible.  It is effective because it reduces the input while preserving semantic validity and avoiding undefined behaviour.
 %It has various reduction strategies, such as delta debugging passes and function inlining, that help it converge rapidly to a test-case that is small enough to understand and step through.
 
-We also check at each stage of the reduction process that the reduced program remains within the subset of the language that is supported by the HLS tools; without this check, \creduce{} only zeroed in on programs that were outside of this subset and hence did not represent real bugs.
+We also check at each stage of the reduction process that the reduced program remains within the subset of the language that is supported by the HLS tools; without this check, we found that \creduce{} kept zeroing in on programs that were outside this subset and hence did not represent real bugs.
 
 %However, the downside of using \creduce{} with HLS tools is that we are not in control of which lines and features are prioritised for removal.
 %As a consequence, we can easily end up with \creduce{} producing programs that are not synthesisable, despite being valid C.