From: Francis Russell Date: Tue, 19 Feb 2013 19:36:25 +0000 (+0000) Subject: Add slides on reasoning about correctness. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=fd6b43994e616d97e74b716dee2be56af86de2c8;p=francis%2Fpsl_presentation_20130225.git Add slides on reasoning about correctness. --- diff --git a/images-svg/simulation_cell.svg b/images-svg/simulation_cell.svg index 085af53..ad2ded6 100644 --- a/images-svg/simulation_cell.svg +++ b/images-svg/simulation_cell.svg @@ -330,14 +330,14 @@ simulation cell + x="590" + y="397.36218">simulation cell diff --git a/presentation.tex b/presentation.tex index d924642..f90349d 100644 --- 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}