Add slides on reasoning about correctness.

diff --git a/images-svg/simulation_cell.svg b/images-svg/simulation_cell.svg
index 085af53d55456cff2ae5dc6451e3f1b67201eb32..ad2ded651e6fd362d2a5c636ec930ac8179bed22 100644 (file)
--- a/images-svg/simulation_cell.svg
+++ b/images-svg/simulation_cell.svg
@@ -330,14 +330,14 @@
     <text
        xml:space="preserve"
        style="font-size:20px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:start;line-height:125%;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;font-family:Nimbus Sans L;-inkscape-font-specification:Nimbus Sans L"
-       x="595"
-       y="467.36218"
+       x="590"
+       y="397.36218"
        id="text4167"
        sodipodi:linespacing="125%"><tspan
          sodipodi:role="line"
          id="tspan4169"
-         x="595"
-         y="467.36218">simulation cell</tspan></text>
+         x="590"
+         y="397.36218">simulation cell</tspan></text>
     <text
        xml:space="preserve"
        style="font-size:20px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;line-height:125%;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;font-family:Nimbus Sans L;-inkscape-font-specification:Nimbus Sans L;text-anchor:start;text-align:start;writing-mode:lr"
@@ -390,7 +390,7 @@
        sodipodi:nodetypes="cc" />
     <path
        style="fill:none;stroke:#000000;stroke-width:2;stroke-linecap:round;stroke-linejoin:miter;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none;marker-end:url(#Arrow2Lend)"
-       d="m 592,462.36218 -88,-58"
+       d="m 585,392.36218 -70,-25"
        id="path5587"
        inkscape:connector-curvature="0"
        sodipodi:nodetypes="cc" />

diff --git a/presentation.tex b/presentation.tex
index d924642ce13558fed30a7c9d217af67aeabfe105..f90349de939244c0fb338d87bb687569e98a61e2 100644 (file)
--- a/presentation.tex
+++ b/presentation.tex
@@ -424,32 +424,24 @@ ways. These include:
 
 \begin{itemize}
 
-\item Up-sampling involves performing an inverse-FFT on data-set padded with
-  zeros (new zero-amplitude frequency components).
+\item Up-sampling involves performing an inverse-FFT on a zero padded data-set (new
+  zero-amplitude frequency components).
 
 \item Down-sampling involves discarding parts of the frequency decomposition
   returned by an FFT (the high-frequency components). 
 
-\item Quite often, a region needing to be upsampled is filled with mostly zeros,
-although the output may be dense and completely fill an FFT box.
+\item Often, a region needing to be upsampled is sparse
+although the output may be dense.
 
 \end{itemize}
 
-}
-
-\frame{
-
-\frametitle{Sparsity in the simulation cell}
-
 \centering
-
-\resizebox{\textwidth}{!}{
+\resizebox{0.85\textwidth}{!}{
 \includegraphics{images-svg/simulation_cell}
 }
 
 }
 
-
 \frame{
 
 \frametitle{Our new approach}
@@ -487,6 +479,83 @@ although the output may be dense and completely fill an FFT box.
 
 }
 
+\frame{
+
+\frametitle{Reasoning about correctness}
+
+The DSL representation that we use as input doesn't contain explicit references
+to the operations used by ONETEP to evaluate these expressions. These include:
+
+\begin{itemize}
+
+  \item Fourier transforms.
+
+  \item Inverse Fourier transforms.
+
+  \item Padding with zeros in the frequency domain.
+
+  \item Truncating data in the frequency domain.
+
+\end{itemize}
+
+We needed a way to correctly infer when to apply these operations. Doing these
+incorrectly could result in calculations that produce invalid data, but are not
+obviously incorrect.
+
+}
+
+\frame{
+
+\frametitle{Reasoning about correctness}
+
+ONETEP handles fields in a similar manner to the digital signal processing
+domain. Things become complicated because:
+
+\begin{itemize}
+
+\item ONETEP will sometimes down-sample data (discard high frequency components)
+  when they are not required.
+
+\item The context in which a signal is used determines the frequency components
+  that must be preserved - this makes it hard to determine how/when
+  data needs to be resampled.
+
+\end{itemize}
+
+We adopt the following strategy:
+
+\begin{itemize}
+
+  \item Generate variants of the expression to be evaluated with up-sampling and
+    down-sampling operations introduced in various locations.
+
+  \item Implement an algorithm that can determine whether or not a given variant
+    preserves the required information. This requires formalising various rules
+    encoded implicitly into ONETEP.
+
+\end{itemize}
+
+}
+
+\frame{
+
+\frametitle{Reasoning about correctness}
+
+\begin{itemize}
+
+  \item Attempting to formalise the rules used by ONETEP has led to the
+    discovery of special edge cases that can occur.
+
+  \item We've developed a system designed to reason about the frequency
+    components of intermediate operands produced in ONETEP.
+
+  \item Applying this system to the generated variants will enable us to
+    determine whether or not a given variant produces a valid answer.
+
+\end{itemize}
+
+}
+
 \end{document}