Update presentation and add references

3 files changed, 118 insertions, 89 deletions

diff --git a/presentation/presentation.org b/presentation/presentation.org
index 3902b42..cce2850 100644
--- a/presentation/presentation.org
+++ b/presentation/presentation.org
@@ -41,7 +41,7 @@ Translation of a high-level programming language such as C/C++ into a hardware d
 High-level synthesis is often quite unreliable:
 
 #+attr_beamer: :overlay <+->
-- When fuzzing OpenCL tools (Lidbury et al.), Intel's OpenCL could not be fuzzed because of *too many issues*.
+- Intel's OpenCL could not be fuzzed because of too many issues (cite:lidbury15_many_core_compil_fuzzin).
 - We fuzzed HLS tools and found they failed on *2.5%* of simple random test cases.
 
 *** HLS Difficulties :B_blockNH:
@@ -50,11 +50,11 @@ High-level synthesis is often quite unreliable:
 :BEAMER_ACT: <3->
 :END:
 
-Debugging HLS tools when they go wrong is difficult:
+Difficult to debug HLS tools:
 
 #+attr_beamer: :overlay <+->
-- It is not clear what part of the input caused the bug.
-- Only testing the input specification is not enough.
+- Simulation can take a long time.
+- Correctness is important in hardware, testing is done at every level.
 
 ** Solution :B_frame:
 :PROPERTIES:
@@ -198,7 +198,7 @@ main() {
 }
 #+end_src
 
-** HTL Overview
+** Example: HTL Overview
 
 The representation of the *finite state-machine with datapath (FSMD)* is abstract and called **HTL**.
 
@@ -272,7 +272,7 @@ Translation from *control-flow graph (CFG)* into a *finite state-machine with da
 
 $\quad\longrightarrow\quad$ ~{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}~
 
-** Memory Inferrence Pass
+** Example: Memory Inference Pass :noexport:
 
 - An HTL $\rightarrow$ HTL translation removes loads and stores.
 - Replaced by accesses to a proper *RAM*.
@@ -461,7 +461,7 @@ endmodule
 - Control logic is translated into another case statement with a reset.
 
 * Verification
-** Verilog Syntax
+** Verilog Syntax :noexport:
 
 *** Column 1 :B_column:
 :PROPERTIES:
@@ -526,15 +526,16 @@ endmodule
 
 #+begin_export latex
 \begin{gather*}
-  \inferrule[Nonblocking]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \downarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])} \quad \inferrule[Blocking]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ = } e) \downarrow_{\text{stmnt}} (\Gamma [n \mapsto v], \Delta)} \\
-  \inferrule[Module]{(\Gamma, \epsilon, \vec{m})\ \downarrow_{\text{module}} (\Gamma', \Delta')}{(\Gamma, \yhkeyword{module } \yhconstant{main} \yhkeyword{(...);}\ \vec{m}\ \yhkeyword{endmodule}) \downarrow_{\text{program}} (\Gamma' // \Delta')}
+%\inferrule[Nonblocking]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \downarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])} \quad \inferrule[Blocking]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ = } e) \downarrow_{\text{stmnt}} (\Gamma [n \mapsto v], \Delta)} \\
+\inferrule[Module]{(\Gamma, \epsilon, \vec{m})\ \downarrow_{\text{module}^{+}} (\Gamma', \Delta') \\ (\Gamma'\ //\ \Delta', \epsilon, \vec{m}) \downarrow_{\text{module}^{-}} (\Gamma'', \Delta'')}{(\Gamma, \yhkeyword{module}\ \yhconstant{main} \yhkeyword{(...);}\ \vec{m}\ \yhkeyword{endmodule}) \downarrow_{\text{program}} (\Gamma''\ //\ \Delta'')}
 \end{gather*}
 #+end_export
 
 #+attr_beamer: :overlay <+->
 - Two separate association maps: current ($\Gamma$) and next ($\Delta$).
 - Maps are merged at the end of the clock cycle.
-** How the Verilog semantics changed
+
+** How the Verilog semantics changed :noexport:
 
 Changed the semantics in *5* minor ways to make it a better HLS target.
 
@@ -620,11 +621,11 @@ This describes the main proof that is needed to show that the HLS tool is correc
 :BEAMER_env: blockNH
 :END:
 
+#+beamer: \vspace{-1.5em}
+
 - We have an *algorithm* describing the *translation*.
 - Have to *prove* that it does not change *behaviour* with respect to our language semantics.
 
-#+beamer: \vspace{1em}
-
 *** Minipage :B_minipage:
 :PROPERTIES:
 :BEAMER_env: minipage
@@ -809,7 +810,54 @@ Fuzzed Vericert with Csmith to check correctness theorem.
 \end{tikzpicture}
 #+end_export
 
-* Extensions
+** Conclusion
+
+Written a formally verified high-level synthesis tool in *Coq* based on *CompCert*.
+
+#+attr_beamer: :overlay <+->
+- Base translation *proven correct* by proving translation of CFG into FSMD.
+- Small optimisations implemented such as *Ram Inference*.
+- Performance without divisions comparable to LegUp without optimisations.
+
+** Thank you :B_fullframe:
+:PROPERTIES:
+:BEAMER_env: fullframe
+:END:
+
+#+begin_export latex
+\begin{center}
+  {\usebeamerfont{frametitle}\Large Thank you\par}
+  {\color{lightgreen}\rule{350pt}{2pt}\par}
+  \vspace{1em}
+  \begin{minipage}{5cm}
+    \begin{center}
+    Documentation\\
+    \includegraphics[width=50pt]{assets/formal_hls_docs.pdf}\\
+    \tiny\url{https://vericert.ymhg.org}
+    \end{center}
+  \end{minipage}
+  \begin{minipage}{5cm}
+  \begin{center}
+  GitHub\\
+  \includegraphics[width=50pt]{assets/formal_hls_github.pdf}\\
+  \tiny\url{https://github.com/ymherklotz/vericert}
+  \end{center}
+  \end{minipage}\vspace{1em}
+  \begin{minipage}{5cm}
+  \begin{center}
+  OOPSLA'21 Preprint\\
+  \includegraphics[width=50pt]{assets/formal_hls_paper.pdf}\\
+  \tiny\url{https://ymhg.org/papers/fvhls_oopsla21.pdf}
+  \end{center}
+  \end{minipage}
+\end{center}
+#+end_export
+** References
+
+bibliography:./references.bib
+
+
+* Extensions :noexport:
 ** Current work
 
 Many optimisations missing:
@@ -867,41 +915,6 @@ Inductive instr: Type :=
 | RBsetpred: condition -> list reg -> predicate -> instr.
 #+end_src
 
-** New passes
-
-#+begin_export latex
-\definecolor{compcert}{HTML}{66c2a5}
-\definecolor{formalhls}{HTML}{fc8d62}
-\begin{center}\scalebox{0.8}{\begin{tikzpicture}[language/.style={fill=white,rounded corners=2pt}]
-    \fill[compcert,rounded corners=3pt] (-1,-1) rectangle (9,1.5);
-    \fill[formalhls,rounded corners=3pt] (-1,-1.5) rectangle (9,-2.5);
-    \node[language] at (0,0) (clight) {Clight};
-    \node[language] at (2,0) (cminor) {C\#minor};
-    \node[language] at (4,0) (rtl) {RTL};
-    \node[language] at (6,0) (ltl) {LTL};
-    \node[language] at (8,0) (ppc) {PPC};
-    \node[language] at (2,-2) (acblock) {\small RTLBlock};
-    \node[language] at (4,-2) (acpar) {\small RTLPar};
-    \node[language] at (6,-2) (dfgstmd) {HTL};
-    \node[language] at (8,-2) (verilog) {Verilog};
-    \node at (0,1) {CompCert};
-    \node at (0,-2) {Vericert};
-    \draw[->] (clight) -- (cminor);
-    \draw[->,dashed] (cminor) -- (rtl);
-    \draw[->] (rtl) -- (ltl);
-    \draw[->,dashed] (ltl) -- (ppc);
-    \draw[->] (rtl) |- (2,-1.3) -- (acblock);
-    \draw[->] (acblock) -- (acpar);
-    \draw[->] (acpar) -- (dfgstmd);
-    \draw[->] (dfgstmd) -- (verilog);
-    \draw[->] ($(acblock.south) - (0.1,0)$) to [out=270,in=180] (2,-3) to [out=0,in=270] ($(acblock.south) + (0.1,0)$);
-\end{tikzpicture}}\end{center}
-#+end_export
-
-#+beamer: \vspace{1em}
-
-Add two more passes, from *RTLBlock* $\rightarrow$ *RTLBlock* and from *RTLBlock* to *RTLPar*.
-
 ** More details of transformations
 
 #+begin_export latex
@@ -1448,48 +1461,41 @@ r_{3}^{0} + r_{3}^{0} + r_{4}^{0} \stackrel{?}{=} r_{3}^{0} + r_{3}^{0} + r_{4}^
 \end{equation*}
 #+end_export
 
-** Conclusion
+** New passes
 
-Written a formally verified high-level synthesis tool in *Coq* based on *CompCert*.
+#+begin_export latex
+\definecolor{compcert}{HTML}{66c2a5}
+\definecolor{formalhls}{HTML}{fc8d62}
+\begin{center}\scalebox{0.8}{\begin{tikzpicture}[language/.style={fill=white,rounded corners=2pt}]
+    \fill[compcert,rounded corners=3pt] (-1,-1) rectangle (9,1.5);
+    \fill[formalhls,rounded corners=3pt] (-1,-1.5) rectangle (9,-2.5);
+    \node[language] at (0,0) (clight) {Clight};
+    \node[language] at (2,0) (cminor) {C\#minor};
+    \node[language] at (4,0) (rtl) {RTL};
+    \node[language] at (6,0) (ltl) {LTL};
+    \node[language] at (8,0) (ppc) {PPC};
+    \node[language] at (2,-2) (acblock) {\small RTLBlock};
+    \node[language] at (4,-2) (acpar) {\small RTLPar};
+    \node[language] at (6,-2) (dfgstmd) {HTL};
+    \node[language] at (8,-2) (verilog) {Verilog};
+    \node at (0,1) {CompCert};
+    \node at (0,-2) {Vericert};
+    \draw[->] (clight) -- (cminor);
+    \draw[->,dashed] (cminor) -- (rtl);
+    \draw[->] (rtl) -- (ltl);
+    \draw[->,dashed] (ltl) -- (ppc);
+    \draw[->] (rtl) |- (2,-1.3) -- (acblock);
+    \draw[->] (acblock) -- (acpar);
+    \draw[->] (acpar) -- (dfgstmd);
+    \draw[->] (dfgstmd) -- (verilog);
+    \draw[->] ($(acblock.south) - (0.1,0)$) to [out=270,in=180] (2,-3) to [out=0,in=270] ($(acblock.south) + (0.1,0)$);
+\end{tikzpicture}}\end{center}
+#+end_export
 
-#+attr_beamer: :overlay <+->
-- Base translation *proven correct*.
-- Some optimisations *implemented*, proofs being worked on.
-- Small issues such as *unsigned comparisons* not working.
+#+beamer: \vspace{1em}
 
-** Thank you :B_fullframe:
-:PROPERTIES:
-:BEAMER_env: fullframe
-:END:
+Add two more passes, from *RTLBlock* $\rightarrow$ *RTLBlock* and from *RTLBlock* to *RTLPar*.
 
-#+begin_export latex
-\begin{center}
-  {\usebeamerfont{frametitle}\Large Thank you\par}
-  {\color{lightgreen}\rule{350pt}{2pt}\par}
-  \vspace{1em}
-  \begin{minipage}{5cm}
-    \begin{center}
-    Documentation\\
-    \includegraphics[width=50pt]{assets/formal_hls_docs.pdf}\\
-    \tiny\url{https://vericert.ymhg.org}
-    \end{center}
-  \end{minipage}
-  \begin{minipage}{5cm}
-  \begin{center}
-  GitHub\\
-  \includegraphics[width=50pt]{assets/formal_hls_github.pdf}\\
-  \tiny\url{https://github.com/ymherklotz/vericert}
-  \end{center}
-  \end{minipage}\vspace{1em}
-  \begin{minipage}{5cm}
-  \begin{center}
-  OOPSLA'21 Preprint\\
-  \includegraphics[width=50pt]{assets/formal_hls_paper.pdf}\\
-  \tiny\url{https://ymhg.org/papers/fvhls_oopsla21.pdf}
-  \end{center}
-  \end{minipage}
-\end{center}
-#+end_export
 ** About Iterative Modulo Scheduling
 
 #+attr_beamer: :overlay <+->
@@ -2072,4 +2078,3 @@ for (int i = 1; i < N - 1; i++) {
 }
 acc[i] = c1 + c2;
 #+end_src
-
diff --git a/presentation/references.bib b/presentation/references.bib
new file mode 100644
index 0000000..98efe04
--- /dev/null
+++ b/presentation/references.bib
@@ -0,0 +1,19 @@
+
+@inproceedings{lidbury15_many_core_compil_fuzzin,
+	author = {Lidbury, Christopher and Lascu, Andrei and Chong, Nathan and Donaldson,
+                  Alastair F.},
+	title = {Many-Core Compiler Fuzzing},
+	booktitle = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation},
+	year = 2015,
+	pages = {65-76},
+	doi = {10.1145/2737924.2737986},
+	url = {https://doi.org/10.1145/2737924.2737986},
+	address = {New York, NY, USA},
+	isbn = 9781450334686,
+	keywords = {random testing, Compilers, OpenCL, metamorphic testing, GPUs, concurrency},
+	location = {Portland, OR, USA},
+	numpages = 12,
+	publisher = {Association for Computing Machinery},
+	series = {PLDI '15}
+}
+
diff --git a/presentation/setup.org b/presentation/setup.org
index 99d8006..8585178 100644
--- a/presentation/setup.org
+++ b/presentation/setup.org
@@ -4,8 +4,10 @@
 #+latex_header: \usepackage{amsmath}
 #+latex_header: \usepackage{mathpartir}
 #+latex_header: \usepackage{booktabs}
-#+latex_header:\usepackage{microtype}
-#+latex_header:\usepackage{mathtools}
+#+latex_header: \usepackage{microtype}
+#+latex_header: \usepackage{mathtools}
+#+latex_header: \usepackage{natbib}
+
 #+latex_header_extra: \DisableLigatures{encoding=T1, family=tt*}
 #+latex_header_extra: \usemintedstyle{manni}
 #+latex_header_extra: \setminted{fontsize=\small}
@@ -20,6 +22,9 @@
 #+latex_header_extra: \newcommand\yhfunctionsp[1]{\;\;\texttt{\textcolor{functioncolour}{#1}}}
 #+latex_header_extra: \newcommand\yhfunction[1]{\texttt{\textcolor{functioncolour}{#1}}}
 #+latex_header_extra: \newcommand\yhconstant[1]{\texttt{\textcolor{constantcolour}{#1}}}
+#+latex_header_extra: \bibliographystyle{plainnat}
+
+#+exclude_tags: noexport
 
 #+beamer_theme: auriga
 #+beamer_color_theme: auriga