Update on Overleaf.

6 files changed, 44 insertions, 26 deletions

diff --git a/conclusion.tex b/conclusion.tex
index d081b09..c5f1f6a 100644
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -1,11 +1,17 @@
 \section{Conclusion}
-We have shown how an existing fuzzing tool can be modified so that its output is suitable for HLS, and then used it in a campaign to test the reliability of three modern HLS tools. In total, we found at least \numuniquebugs{} unique bugs across all the tools, including both crashes and miscompilations. 
-Further work could be done on supporting more HLS tools, especially ones that claim to prove that their output is correct before terminating, such as Catapult-C~\cite{mentor20_catap_high_level_synth}. % This could give an indication of how effective these proofs are, and how often they are actually able to complete their equivalence proofs during compilation in a feasible timescale.
+We have shown how an existing fuzzing tool can be modified so that its output is suitable for HLS, and then used it in a campaign to test the reliability of four modern HLS tools. In total, we found at least \numuniquebugs{} unique bugs across all the tools, including both crashes and miscompilations. 
+Further work could be done on supporting more HLS tools, especially those that claim to prove that their output is correct before terminating, such as Catapult-C~\cite{mentor20_catap_high_level_synth}. % This could give an indication of how effective these proofs are, and how often they are actually able to complete their equivalence proofs during compilation in a feasible timescale.
 
 Conventional compilers have become quite resilient to fuzzing over the last decade, so recent work on fuzzing compilers has had to employ increasingly imaginative techniques to keep finding new bugs~\cite{karine+20}. In contrast, we have found that HLS tools -- at least, as they currently stand -- can be made to exhibit bugs even using the relatively basic fuzzing techniques that we employed in this project.
 
 As HLS is becoming increasingly relied upon, it is important to make sure that HLS tools are also reliable.  We hope that this work further motivates the need for rigorous engineering of HLS tools, whether that is by validating that each output the tool produces is correct or by proving the HLS tool itself correct once and for all.
 
+\section*{Acknowledgements}
+
+We thank Alastair F. Donaldson for helpful feedback. 
+We acknowledge financial support from the Research Institute on Verified Trustworthy Software Systems (VeTSS), which is funded by the UK National Cyber Security Centre (NCSC).
+
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "main"
diff --git a/eval.tex b/eval.tex
index 312ed25..88ab6a1 100644
--- a/eval.tex
+++ b/eval.tex
@@ -51,14 +51,16 @@ We tested one version of Intel i++ (included in Quartus Lite 18.1), LegUp (4.0)
 \end{figure}
 
 Figure~\ref{fig:existing_tools} shows an Euler diagram of our results. 
-We see that 918 (13.7\%), 167 (2.5\%), 83 (1.2\%) and 26 (0.4\%) test-cases fail in Bambu, LegUp, Vivado HLS and Intel i++ respectively.  However, one of the bugs in Bambu was fixed as we were testing the tool, so we therefore tested the development branch of Bambu (0.9.7-dev) with that bug fix, and only found 17 (0.25\%) remaining failing test-cases.
-Despite i++ having the lowest failure rate, it has the highest time-out rate (540 test-cases), because of its remarkably long compilation time, whereas the other tools each only had under 20 test-cases timeout.
-Note that the absolute numbers here do not necessarily correspond to the number of bugs in the tools, because a single bug in a language feature that appears frequently in our test suite could cause many programs to crash or fail.
-Moreover, we are reluctant to draw conclusions about the relative reliability of each tool by comparing the number of test-case failures, because these numbers are so sensitive to the parameters of the randomly generated test suite we used. In other words, we can confirm the \emph{presence} of bugs, but cannot deduce the \emph{number} of them (nor their importance).
+We see that 918 (13.7\%), 167 (2.5\%), 83 (1.2\%) and 26 (0.4\%) test-cases fail in Bambu, LegUp, Vivado HLS and Intel i++ respectively.  One of the bugs we reported to the Bambu developers was fixed during our testing campaign, so we also tested the development branch of Bambu (0.9.7-dev) with the bug fix, and found only 17 (0.25\%) failing test-cases.
+Although i++ has a low failure rate, it has the highest time-out rate (540 test-cases) due to its remarkably long compilation time. No other tool had more than 20 time-outs.
+Note that the absolute numbers here do not necessarily correspond to the number of bugs in the tools, because a single bug in a language feature that appears frequently in our test suite could cause many failures.
+Moreover, we are reluctant to draw conclusions about the relative reliability of each tool by comparing the number of failures, because these numbers are so sensitive to the parameters of the randomly generated test suite we used. In other words, we can confirm the \emph{presence} of bugs, but cannot deduce the \emph{number} of them (nor their importance).
 
 We have reduced several of the failing test-cases in an effort to identify particular bugs, and our findings are summarised in Table~\ref{tab:bugsummary}. We emphasise that the bug counts here are lower bounds -- we did not have time to go through the arduous test-case reduction process for every failure.
 Figures~\ref{fig:eval:legup:crash}, \ref{fig:eval:intel:mismatch}, and~\ref{fig:eval:bambu:mismatch} present three of the bugs we found. As in Example~\ref{ex:vivado_miscomp}, each bug was first reduced automatically using \creduce{}, and then further reduced manually to achieve the minimal test-case.
 
+% \AD{Could spell out why it's so arduous -- involves testing an enormous number of programs and each one takes ages.} \JW{I'd be inclined to leave this as-is, actually.}
+
 \begin{figure}
 \begin{minted}{c}
 int a[2][2][1] = {{{0},{1}},{{0},{0}}};
@@ -157,15 +159,16 @@ int main() {
     \textbf{Tool} & \textbf{Bug type} & \textbf{Details} & \textbf{Status} \\
     \midrule
     Vivado HLS & miscompile & Fig.~\ref{fig:vivado_bug1} & reported, confirmed \\
-    Vivado HLS & miscompile & webpage & reported \\
+    Vivado HLS & miscompile & online* & reported \\
     LegUp HLS & crash & Fig.~\ref{fig:eval:legup:crash} & reported \\
-    LegUp HLS & crash & webpage & reported \\
-    LegUp HLS & miscompile & webpage & reported, confirmed \\
+    LegUp HLS & crash & online* & reported \\
+    LegUp HLS & miscompile & online* & reported \\
     Intel i++ & miscompile & Fig.~\ref{fig:eval:intel:mismatch} & reported \\
     Bambu HLS & miscompile & Fig.~\ref{fig:eval:bambu:mismatch} & reported, confirmed, fixed \\
-    Bambu HLS & miscompile & webpage & reported, confirmed \\
+    Bambu HLS & miscompile & online* & reported, confirmed \\
     \bottomrule
-  \end{tabular}
+  \end{tabular} \\
+  \vphantom{\large A}*See \url{https://ymherklotz.github.io/fuzzing-hls/} for detailed bug reports
 \end{table}
 
 %We write `$\ge$' above to emphasise that all the bug counts are lower bounds -- we did not have time to go through the rather arduous test-case reduction process for every failure.
@@ -218,8 +221,10 @@ int main() {
 Besides studying the reliability of different HLS tools, we also studied the reliability of Vivado HLS over time. Figure~\ref{fig:sankey_diagram} shows the results of giving \vivadotestcases{} test-cases to Vivado HLS v2018.3, v2019.1 and v2019.2. 
 Test-cases that pass and fail in the same tools are grouped together into a ribbon. 
 For instance, the topmost ribbon represents the 31 test-cases that fail in all three versions of Vivado HLS. Other ribbons can be seen weaving in and out; these indicate that bugs were fixed or reintroduced in the various versions. We see that Vivado HLS v2018.3 had the most test-case failures (62).
-Interestingly, the blue ribbon shows that there are test-cases that fail in v2018.3, pass in v2019.1, and then fail again in v2019.2.
-As in our Euler diagram, the numbers do not necessary correspond to the number of actual bugs, though we can observe that there must be at least six unique bugs in Vivado HLS, given that each ribbon corresponds to at least one unique bug.
+Interestingly, the blue ribbon shows that there are test-cases that fail in v2018.3, pass in v2019.1, and then fail again in v2019.2!
+As in our Euler diagram, the numbers do not necessary correspond to the number of actual bugs, though we can observe that there must be at least six unique bugs in Vivado HLS, given that each ribbon corresponds to at least one unique bug. 
+
+%\AD{This reminds me of the correcting commits metric from Junjie Chen et al.'s empirical study on compiler testing. Could be worth making the connection. }
 
 %\YH{Contradicts value of 3 in Table~\ref{tab:unique_bugs}, maybe I can change that to 6?} \JW{I'd leave it as-is personally; we have already put a `$\ge$' symbol in the table, so I think it's fine.}
 %In addition to that, it can then be seen that Vivado HLS v2018.3 must have at least 4 individual bugs, of which two were fixed and two others stayed in Vivado HLS v2019.1.  However, with the release of v2019.1, new bugs were introduced as well. % Finally, for version 2019.2 of Vivado HLS, there seems to be a bug that was reintroduced which was also present in Vivado 2018.3, in addition to a new bug.  In general it seems like each release of Vivado HLS will have new bugs present, however, will also contain many previous bug fixes.  However, it cannot be guaranteed that a bug that was previously fixed will remain fixed in future versions as well.
diff --git a/intro.tex b/intro.tex
index 4432fc1..0ceab4e 100644
--- a/intro.tex
+++ b/intro.tex
@@ -1,7 +1,7 @@
 \section{Introduction}
 
-High-level synthesis (HLS), which refers to the automatic translation of software into hardware, is becoming an increasingly important part of the computing landscape, even in such high-assurance settings as financial services~\cite{hls_fintech}, control systems~\cite{hls_controller}, and real-time object detection~\cite{hls_objdetect}.
-The appeal of HLS is twofold: it promises hardware engineers an increase in productivity by raising the abstraction level of their designs, and it promises software engineers the ability to produce application-specific hardware accelerators without having to understand Verilog and VHDL.
+High-level synthesis (HLS), which refers to the automatic translation of software into hardware, is becoming an important part of the computing landscape, even in such high-assurance settings as financial services~\cite{hls_fintech}, control systems~\cite{hls_controller}, and real-time object detection~\cite{hls_objdetect}.
+The appeal of HLS is twofold: it promises hardware engineers an increase in productivity by raising the abstraction level of their designs, and it promises software engineers the ability to produce application-specific hardware accelerators without having to understand Verilog or VHDL.
 
 As such, we are increasingly reliant on HLS tools. But are these tools reliable? Questions have been raised about the reliability of HLS before; for example, Andrew Canis, co-creator of the LegUp HLS tool, wrote that ``high-level synthesis research and development is inherently prone to introducing bugs or regressions in the final circuit functionality''~\cite[Section 3.4.6]{canis15_legup}. In this paper, we investigate whether there is substance to this concern by conducting an empirical evaluation of the reliability of several widely used HLS tools.
 
@@ -50,7 +50,7 @@ int main() {
   \label{fig:vivado_bug1}
 \end{figure}
 
-The example above demonstrates the effectiveness of fuzzing. It seems unlikely that a human-written test-suite would discover this particular bug, given that it requires several components all to coincide before the bug is revealed!
+The example above demonstrates the effectiveness of fuzzing. It seems unlikely that a human-written test-suite would discover this particular bug, given that it requires several components all to coincide before the bug is revealed. If the loop is unrolled, or the seemingly random value of \code{b} is simplified, or the array is declared with fewer than six elements (even though only two are accessed), then the bug goes away.
 
 Yet this example also begs the question: do bugs found by fuzzers really \emph{matter}, given that they are usually found by combining language features in ways that are vanishingly unlikely to happen `in the real world'~\cite{marcozzi+19}. This question is especially pertinent for our particular context of HLS tools, which are well-known to have restrictions on the language features they support. Nevertheless, although the \emph{test-cases} we generated do not resemble the programs that humans write, the \emph{bugs} that we exposed using those test-cases are real, and \emph{could also be exposed by realistic programs}.
 %Moreover, it is worth noting that HLS tools are not exclusively provided with human-written programs to compile: they are often fed programs that have been automatically generated by another compiler.
@@ -61,9 +61,11 @@ Ultimately, we believe that any errors in an HLS tool are worth identifying beca
 Our approach to fuzzing HLS tools comprises three steps. 
 First, we use Csmith~\cite{yang11_findin_under_bugs_c_compil} to generate thousands of valid C programs within the subset of the C language that is supported by all the HLS tools we test. We also augment each program with a random selection of HLS-specific directives. Second, we give these programs to four widely used HLS tools: Xilinx Vivado HLS~\cite{xilinx20_vivad_high_synth}, LegUp HLS~\cite{canis13_legup}, the Intel HLS Compiler, also known as i++~\cite{intel20_sdk_openc_applic}, and finally Bambu~\cite{pilato13_bambu}. Third, if we find a program that causes an HLS tool to crash or to generate hardware that produces a different result from GCC, we reduce it to a minimal example with the help of \creduce{}~\cite{creduce}.
 
-Our testing campaign revealed that all four tools could be made to generate an incorrect design.  In total, \totaltestcases{} test-cases were run through each tool, of which \totaltestcasefailures{} failed in at least one of the tools.  Test-case reduction was then performed on some of these failing test-cases to obtain at least \numuniquebugs{} unique failing test-cases.
+Our testing campaign revealed that all four tools could be made to generate an incorrect design.  In total, \totaltestcases{} test-cases were run through each tool, of which \totaltestcasefailures{} failed in at least one of the tools.  Test-case reduction was then performed on some of these failing test-cases to obtain at least \numuniquebugs{} unique failing test-cases, detailed on our companion webpage: \begin{center}
+    \url{https://ymherklotz.github.io/fuzzing-hls/}
+\end{center}
     
-To investigate whether HLS tools are getting more or less reliable over time, we also tested three different versions of Vivado HLS (v2018.3, v2019.1, and v2019.2).  We found far fewer failures in versions v2019.1 and v2019.2 compared to v2018.3, but we also identified a few test-cases that only failed in versions v2019.1 and v2019.2; this suggests that some new features may have introduced bugs.
+To investigate whether HLS tools are getting more or less reliable, we also tested three different versions of Vivado HLS (v2018.3, v2019.1, and v2019.2).  We found fewer failures in v2019.1 and v2019.2 compared to v2018.3, but also identified a few test-cases that only failed in v2019.1 and v2019.2; this suggests that new features may have introduced bugs.
 
 In summary, the overall aim of our paper is to raise awareness about the reliability (or lack thereof) of current HLS tools, and to serve as a call-to-arms for investment in better-engineered tools. We hope that future work on developing more reliable HLS tools will find our empirical study a valuable source of motivation.
 
diff --git a/main.tex b/main.tex
index ff9e1e2..5671dc9 100644
--- a/main.tex
+++ b/main.tex
@@ -23,7 +23,7 @@
 %\usepackage{balance}
 
 \newcommand\totaltestcases{6700}
-\newcommand\totaltestcasefailures{1178}
+\newcommand\totaltestcasefailures{1191}
 \newcommand\numuniquebugs{8}
 \newcommand\vivadotestcases{3645}
 
@@ -32,6 +32,7 @@
 
 \newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [[#2:} #3{\bf ]]}}\fi}
 \newcommand\JW[1]{\Comment{red!75!black}{JW}{#1}}
+\newcommand\AD[1]{\Comment{yellow!50!black}{AD}{#1}}
 \newcommand\YH[1]{\Comment{green!50!blue}{YH}{#1}}
 \newcommand\NR[1]{\Comment{yellow!50!black}{NR}{#1}}
 \newcommand\ZD[1]{\Comment{blue!50!black}{NR}{#1}}
@@ -58,8 +59,8 @@ Email: \{yann.herklotz15, zewei.du19, n.ramanathan14, j.wickerson\}@imperial.ac.
 High-level synthesis (HLS) is becoming an increasingly important part of the computing landscape, even in safety-critical domains where correctness is key. 
 As such, HLS tools are increasingly relied upon. But are they trustworthy?
 
-We have subjected four widely used HLS tools -- LegUp, Xilinx Vivado HLS, the Intel HLS Compiler and Bambu -- to a rigorous fuzzing campaign using thousands of random, valid C programs that we generated using a modified version of the Csmith tool. For each C program, we compiled it to a hardware design using the HLS tool under test and checked whether that hardware design generates the same output as an executable generated by the GCC compiler. When discrepancies arose between GCC and the HLS tool under test, we reduced the C program to a minimal example in order to zero in on the potential bug. Our testing campaign has revealed that all four HLS tools can be made either to crash or to generate wrong code when given valid C programs, and thereby underlines the need for these increasingly trusted tools to be more rigorously engineered.
-Out of \totaltestcases{} test-cases, we found \totaltestcasefailures{} programs that failed in at least one tool, out of which we were able to discern at least \numuniquebugs{} unique bugs.
+We have subjected four widely used HLS tools -- LegUp, Xilinx Vivado HLS, the Intel HLS Compiler and Bambu -- to a rigorous fuzzing campaign using thousands of random, valid C programs that we generated using a modified version of the Csmith tool. For each C program, we compiled it to a hardware design using the HLS tool under test and checked whether that hardware design generates the same output as an executable generated by the GCC compiler. When discrepancies arose between GCC and the HLS tool under test, we reduced the C program to a minimal example in order to zero in on the potential bug. Our testing campaign has revealed that all four HLS tools can be made to generate wrong designs and one tool could be made to crash when given valid C programs, which thereby underlines the need for these increasingly trusted tools to be more rigorously engineered.
+Out of \totaltestcases{} test-cases, we found \totaltestcasefailures{} programs that caused at least one tool to fail, out of which we were able to discern at least \numuniquebugs{} unique bugs.
 
 \end{abstract}
 
diff --git a/method.tex b/method.tex
index 398a97d..c377c3e 100644
--- a/method.tex
+++ b/method.tex
@@ -120,9 +120,11 @@ We avoid floating-point numbers since these often involve external libraries or
 %\subsection{Augmenting programs for HLS testing}
 %\label{sec:method:annotate}
 
-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.
+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 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.
+%\AD{Did any reduced test-case involve these HLS-specific features?} \JW{The LegUp bug in Figure 4 requires NO\_INLINE -- does that count? If so, perhaps we could append to the Figure 4 caption: `thus vindicating our strategy of adding random HLS directives to our test-cases'.}
+
+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, hoping that miscompilations will be exposed through this hash value. Csmith's built-in hash function leads to infeasibly long synthesis times, so we replace it with a 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.
 
diff --git a/related.tex b/related.tex
index 208f1fc..47f1a08 100644
--- a/related.tex
+++ b/related.tex
@@ -1,14 +1,16 @@
 \section{Related Work}
 
-The only other work of which we are aware on fuzzing HLS tools is that by Lidbury et al. \cite{lidbury15_many_core_compil_fuzzin}, who tested several OpenCL compilers, including an HLS compiler from Altera (now Intel). They were only able to subject that compiler to superficial testing because so many of the test-cases they generated led to it crashing. In comparison to our work: where Lidbury et al. generated target-independent OpenCL programs that could be used to test HLS tools and conventional compilers alike, we specifically generate programs that are tailored for HLS (e.g. with HLS-specific pragmas and only including supported constructs) with the aim of testing the HLS tools more deeply. Another difference is that where we test using sequential C programs, they test using highly concurrent OpenCL programs, and thus have to go to great lengths to ensure that any discrepancies observed between compilers cannot be attributed to the inherent nondeterminism of concurrency.
+The only other work of which we are aware on fuzzing HLS tools is that by Lidbury et al. \cite{lidbury15_many_core_compil_fuzzin}, who tested several OpenCL compilers, including an HLS compiler from Altera (now Intel). They were only able to subject that compiler to superficial testing because so many of the test-cases they generated led to it crashing. In comparison to our work: where Lidbury et al. generated target-independent OpenCL programs for testing HLS tools and conventional compilers alike, we generate programs that are tailored for HLS (e.g. with HLS-specific pragmas and only including supported constructs) with the aim of testing the HLS tools more deeply. Another difference is that where we test using sequential C programs, they test using highly concurrent OpenCL programs, and thus have to go to great lengths to ensure that any discrepancies observed between compilers cannot be attributed to the inherent nondeterminism of concurrency.
 
 Other stages of the FPGA toolchain have been subjected to fuzzing. In previous work~\cite{verismith}, we tested several FPGA synthesis tools using randomly generated Verilog programs. Where that work concentrated on the RTL-to-netlist stage of hardware design, this work focuses on the C-to-RTL stage.
 
 Several authors have taken steps toward more rigorously engineered HLS tools that may be more resilient to testing campaigns such as ours. 
-The Handel-C compiler by Perna and Woodcock~\cite{perna12_mechan_wire_wise_verif_handel_c_synth} has been mechanically proven correct, at least in part, using the HOL theorem prover; however, the tool does not support C as input directly, so is not amenable to fuzzing. 
+The Handel-C compiler by Perna and Woodcock~\cite{perna12_mechan_wire_wise_verif_handel_c_synth} has been mechanically proven correct, at least in part, using the HOL theorem prover; however, the tool does not support C as input, so is not amenable to fuzzing. 
 Ramanathan et al.~\cite{ramanathan+17} proved their implementation of C atomic operations in LegUp correct up to a bound using model checking; however, our testing campaign is not applicable to their implementation because we do not generate concurrent C programs.
 In the SPARK HLS tool~\cite{gupta03_spark}, some compiler passes, such as scheduling, are mechanically validated during compilation~\cite{chouksey20_verif_sched_condit_behav_high_level_synth}; unfortunately, this tool is no longer available.
-Finally, the Catapult C HLS tool~\cite{mentor20_catap_high_level_synth} is designed only to produce an output netlist if it can mechanically prove it equivalent to the input program; it should therefore never produce wrong RTL. In future work, we intend to test Catapult C alongside Vivado HLS, LegUp, Intel i++, and Bambu.
+Finally, the Catapult C HLS tool~\cite{mentor20_catap_high_level_synth} is designed only to produce an output netlist if it can mechanically prove it equivalent to the input program; it should therefore never produce wrong RTL. In future work, we intend to test Catapult C alongside Vivado HLS, LegUp, Intel i++, and Bambu. 
+%\AD{Is there a good reason why we didn't prioritise Catapult C yet?}
+% YH: not really
 %more prevalent these were prioritised.
 % JW: We're not really sure that LegUp is more prevalent than Catapult HLS. Indeed, it probably isn't!
 %\JW{Obvious reader question at this point: why not test that claim by giving our Csmith test-cases to Catapult C too? Can we address that here? No worries if not; but shall we try and do that after the deadline anyway?}\YH{Yes, definitely, it would be great to get an idea of how Catapult C performs, and I currently have it installed already.  I have added a small sentence for that now, but let me know if I should mention this in the conclusion instead though. }