Doop doop doop. Some contribution writing stuff.

1 files changed, 335 insertions, 0 deletions

diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
new file mode 100644
index 0000000..8a09c0a
--- /dev/null
+++ b/tex/thesis/contribution/contribution.tex
@@ -0,0 +1,335 @@
+\chapter{Contribution} \label{chap:contribution}
+
+The main theoretical contribution of this paper is an improvement on
+the algorithm presented in \cite{Gawlitza:2007:PFC:1762174.1762203}
+for solving fixpoint equations over the integers with monotonic
+operators. The algorithm is presented in section
+\ref{section:basic-algorithm}.
+
+The algorithm consists of two iterative operations: fixpoint iteration
+and max-strategy iteration. Each of these operations can be made
+significantly faster by the application of the algorithms presented in
+\cite{DBLP:tr/trier/MI96-11}. In particular the algorithm W-DFS (which
+is alluded to in \cite{DBLP:tr/trier/MI96-11} and presented in
+\cite{fixpoint-slides}) provides a considerable speed up by taking
+into account dynamic dependency information to minimise the number of
+re-evaluations that must be done. The W-DFS algorithm is presented as
+algorithm \ref{algo:w-dfs}.
+
+
+\section{W-DFS}
+
+\subsection{Fixpoint Iteration}
+
+\newcommand\stable{\mathsf{stable}}
+\newcommand\eval{\mathsf{eval}}
+\newcommand\solve{\mathsf{solve}}
+\newcommand\system{\mathsf{system}}
+\algblockx[Globals]{Globals}{EndGlobals}{\textbf{Globals:\\}}{} 
+
+\begin{algorithm}
+  \begin{algorithmic}
+    \Globals
+    \begin{tabular}{rl}
+      D & A mapping from variables to their current values, starting
+      at $\{ x \mapsto \infty | \forall x \in X \}$ \\ 
+      I & A mapping from a variable to the variables which depend on
+      it in their evaluation \\
+      stable & The set of all variables whose values have stabilised \\ 
+      system & The equation system, a mapping from a variable to its
+      associated function \\
+    \end{tabular}
+    \EndGlobals
+
+    \Function {eval} {$x$, $y$}
+    \Comment{Evaluate $y$ for its value and note that when $y$
+      changes, $x$ must be re-evaluated}
+      \State $\solve(y)$
+      \State $I[y] = I[y] \cup \{x\}$
+      \State \Return $D[y]$
+    \EndFunction
+
+    \Function {solve} {$x$}
+    \Comment{Solve a specific variable and place its value in $D$}
+    \If {$x \not \in \stable$}
+      \State $f = \system[x]$
+      \State $\stable = \stable \cup \{x\}$
+      \State $v = f( \lambda y . \eval(x, y) )$
+      \If {$v \ne D[x]$}
+        \State $D = \{ x \mapsto v, \alpha \mapsto D[\alpha] \}
+        \forall \alpha \ne x$
+        \State $W = I[x]$
+        \State $I(x) = \emptyset$
+        \State $\stable = \stable \backslash W$
+        \For {$v \in W$}
+          \State $\solve(v)$
+        \EndFor
+      \EndIf
+    \EndIf
+    \EndFunction
+  \end{algorithmic}
+
+  \caption{The W-DFS alluded to in \cite{DBLP:tr/trier/MI96-11} and
+    presented in \cite{fixpoint-slides}, modified to find
+    greatest-fixpoints of monotonic fixpoint equations}
+  \label{algo:w-dfs}
+\end{algorithm}
+
+W-DFS can be used to quickly find the solutions to systems of fixpoint
+equations and, in the case of monotonic right hand sides, will always
+return the least fixpoint. The algorithm also functions
+\emph{locally}, only taking into account the subset of the equation
+system that it is necessary to examine to solve for the requested
+variable's value.
+
+One simple modification to the presented algorithm for solving a
+system of equations involving $\max$- and $\min$-expressions is to
+replace the Bellman-Ford sub-procedure with the W-DFS fixpoint
+solver. This alone can give a considerable speed increase by reducing
+the amount of work to be done in each $\max$-strategy iteration step.
+
+Another simple optimisation can be to utilise the W-DFS algorithm to
+speed up the max-strategy iteration. This optimisation is not as
+obvious as using W-DFS to solve the fixpoint-iteration step, so some
+justification is necessary.
+
+\subsection{Max-Strategy Iteration}
+
+The $\max$-strategy iteration can be viewed as a fixpoint problem. We
+are attempting to find a strategy, $\sigma: E_{\max} \to E$ that will
+result in the greatest value for each $e \in E_{\max}$. Therefore if
+we consider our ``variables'' to be $\max$-expressions, our ``values''
+to be their subexpressions and our ``comparison'' to be carried out
+using the result of evaluating the system with that strategy.
+
+This, then, allows us to use the W-DFS algorithm to re-evaluate only
+those parts of the strategy which have changed. Algorithm
+\ref{algo:w-dfs-max} presents this variation on W-DFS.
+
+\begin{algorithm}
+  \begin{algorithmic}
+    \Globals
+    \begin{tabular}{rl}
+      $\sigma$ & A mapping from $\max$-expressions to their current
+      sub-expressions, starting by \\& mapping to the first
+      sub-expression \\
+      I & A mapping from a $\max$-expression to the sub-expressions
+      which depend on it \\& in their evaluation \\
+      stable & The set of all $\max$-expressions whose strategies have
+      stabilised \\
+      system & The equation system, a mapping from a variable to its
+      associated function \\
+      bestStrategy & A function $(E_{\max}, (X \to D)) \to E$ mapping
+      from an expression and a variable \\& assignment to the greatest
+      subexpression in that context
+    \end{tabular}
+    \EndGlobals
+
+    \Function {eval} {$x$, $y$}
+    \Comment{Evaluate $y$ for its value and note that when $y$
+      changes, $x$ must be re-evaluated}
+      \State $\solve(y)$
+      \State $I[y] = I[y] \cup \{x\}$
+      \State \Return $\sigma[y]$
+    \EndFunction
+
+    \Function {solve} {$x$}
+    \Comment{Solve a specific expression and place its value in $\sigma$}
+    \If {$x \not \in \stable$}
+      \State $f = \system[x]$
+      \State $\stable = \stable \cup \{x\}$
+      \State $v = bestStrategy(x, \lambda y . \eval(x, y))$
+      \If {$v \ne \sigma[x]$}
+        \State $\sigma = \{ x \mapsto v, \alpha \mapsto \sigma[\alpha]
+        \} \forall \alpha \ne x $
+        \State $W = I[x]$
+        \State $I(x) = \emptyset$
+        \State $\stable = \stable \backslash W$
+        \For {$v \in W$}
+        \State $\solve(v)$
+        \EndFor
+      \EndIf
+    \EndIf
+    \EndFunction
+  \end{algorithmic}
+
+  \caption{W-DFS, this time modified to find the best $\max$-strategy.}
+  \label{algo:w-dfs-max}
+\end{algorithm}
+
+
+\section{Combined W-DFS}
+
+W-DFS can be used to speed up both the $\max$-strategy iteration and
+the fixpoint iteration as two independent processes, but each
+fixpoint-iteration step still requires at least one complete
+evaluation of the equation system per $\max$-strategy improvement
+step. Ideally we would be able to adapt the W-DFS algorithm so that
+the fixpoint-iteration and $\max$-strategy iteration steps could
+provide some information to each other about what values have changed
+so that at each step only a subset of the entire system would have to
+be evaluated.
+
+The new algorithm, \emph{Combined W-DFS} seeks to do this. By adding
+an ``invalidate'' method to both W-DFS instances we provide an
+interface for the two sides of the algorithm to indicate which values
+have changed. This gives the other side enough information to avoid
+evaluating irrelevant portions of the equation system.
+
+This algorithm is presented in two parts. Algorithm
+\ref{algo:combined-fixpoint} presents the fixpoint-iteration portion
+of the algorithm, while \ref{algo:combined-max} presents the
+$\max$-strategy portion.  The correctness of this new algorithm is
+argued in \ref{sec:combined-correctness}.
+
+
+\begin{algorithm}
+  \begin{algorithmic}
+    \Globals
+    \begin{tabular}{rl}
+      D & A mapping from variables to their current values, starting
+      at $\{ x \mapsto \infty \}$ \\ 
+      I & A mapping from a variable to the variables which depend on
+      it in their evaluation \\
+      stable & The set of all variables whose values have stabilised \\ 
+      system & The equation system, a mapping from a variable to its
+      associated function \\
+    \end{tabular}
+    \EndGlobals
+
+    \Function {eval} {$x$, $y$}
+    \Comment{Evaluate $y$ for its value and note that when $y$
+      changes, $x$ must be re-evaluated}
+      \State $\solve(y)$
+      \State $I[y] = I[y] \cup \{x\}$
+      \State \Return $D[y]$
+    \EndFunction
+
+    \Function {invalidate} {$x$}
+    \If {$x \in \stable$}
+      \State $\stable = \stable \backslash \{x\}$
+      \State $D[x] = \infty$
+      \State $W = I[x]$
+      \State $I[x] = \emptyset$
+      \For {$v \in W$}
+        invalidate(v)
+      \EndFor
+    \EndIf
+    \EndFunction
+
+    \Function {solve} {$x$}
+    \Comment{Solve a specific expression and place its value in $D$}
+    \If {$x \not \in \stable$}
+      \State $f = \system[x]$
+      \State $\stable = \stable \cup \{x\}$
+      \State $v = f( \lambda y . \eval(x, y) )$
+      \If {$v \ne D[x]$}
+        \State $D = \{ x \mapsto v, \alpha \mapsto D[\alpha] \}
+        \forall \alpha \ne x$
+        \State $W = I[x]$
+        \State $I(x) = \emptyset$
+        \State strategy::invalidate($x$)
+        \State $\stable = \stable \backslash W$
+        \For {$v \in W$}
+        \State $\solve(v)$
+        \EndFor
+      \EndIf
+    \EndIf
+    \EndFunction
+  \end{algorithmic}
+
+  \caption{The fixpoint portion of the Combined W-DFS.}
+  \label{algo:combined-fixpoint}
+\end{algorithm}
+
+
+\begin{algorithm}
+  \begin{algorithmic}
+    \Globals
+    \begin{tabular}{rl}
+      $\sigma$ & A mapping from $\max$-expressions to their current
+      sub-expressions, starting by \\& mapping to the first
+      sub-expression \\
+      D & A \emph{dynamic} variable assignment which will stay updated
+      as $\sigma$ changes \\
+      $I$ & A mapping from a $\max$-expression to the sub-expressions
+      which depend on it \\& in their evaluation \\
+      $I_V$ & A mapping from a variable to the $\max-$ expressions which
+      depend on it in their \\& evaluation \\
+      stable & The set of all $\max$-expressions whose strategies have
+      stabilised \\
+      system & The equation system, a mapping from a variable to its
+      associated function \\
+      bestStrategy & A function $(E_{\max}, (X \to D)) \to E$ mapping
+      from an expression and a variable \\& assignment to the greatest
+      subexpression in that context
+    \end{tabular}
+    \EndGlobals
+
+    \Function {eval} {$x$, $y$}
+    \Comment{Evaluate $y$ for its value and note that when $y$
+      changes, $x$ must be re-evaluated}
+      \State $\solve(y)$
+      \State $I[y] = I[y] \cup \{x\}$
+      \State \Return $\sigma[y]$
+    \EndFunction
+
+    \Function {invalidate} {$x \in X$} \Comment{X is vars}
+      \State $\stable = \stable \backslash I[x]$
+      \State $W = I_v[x]$
+      \State $I_V = \emptyset$
+      \For {$v \in W$}
+        \State solve(v)
+      \EndFor
+    \EndFunction
+
+    \Function {solve} {$x$}
+    \Comment{Solve a specific variable and place its value in $\sigma$}
+    \If {$x \not \in \stable$}
+      \State $f = \system[x]$
+      \State $\stable = \stable \cup \{x\}$
+      \State $v = bestStrategy(x,
+                               \lambda y . \eval(x, y))$
+      \If {$v \ne \sigma[x]$}
+        \State $\sigma = \{ x \mapsto v, \alpha \mapsto \sigma[\alpha]
+        \} \forall \alpha \ne x $
+        \State $W = I[x]$
+        \State $I(x) = \emptyset$
+        \State fixpoint::invalidate$(\mathsf{lookupVarFor}(x))$
+        \State $\stable = \stable \backslash W$
+        \For {$v \in W$}
+          \State $\solve(v)$
+        \EndFor
+      \EndIf
+    \EndIf
+    \EndFunction
+  \end{algorithmic}
+
+  \caption{The $\max$-strategy portion of the Combined W-DFS.}
+  \label{algo:combined-max}
+\end{algorithm}
+
+
+\subsection{Correctness} \label{sec:combined-correctness}
+
+This algorithm relies on the correctness of the underlying W-DFS
+algorithm. This algorithm was presented in
+\cite{DBLP:tr/trier/MI96-11}.
+
+If we assume that W-DFS is correct then we only have to prove that the
+combination algorithm is correct. For this it is sufficient to show
+that the invalidate calls in both directions preserve the correctness
+of the original algorithm.
+
+// TODO finish this.
+General idea:
+\begin{itemize}
+  \item
+    Invalidate calls from fixpoint $\to$ max strategy are correct if
+    the calls the other way are, because it completely re-solves the
+    equations
+  \item
+    Invalidate calls from max strategy $\to$ fixpoint are correct
+    because they effectively ``reset'' that part of the system,
+    creating it to be entirely re-calculated.
+\end{itemize}