More work on the thesis itself.

1 files changed, 141 insertions, 53 deletions

diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index 8a09c0a..6d4aeca 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -1,54 +1,153 @@
-\chapter{Contribution} \label{chap:contribution}
+\floatname{algorithm}{Listing}
 
-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}.
+\newcommand\stable{\mathsf{stable}}
+\newcommand\eval{\mathsf{\textsc{eval}}}
+\newcommand\solve{\mathsf{\textsc{solve}}}
+\newcommand\system{\mathsf{system}}
+\algblockx[Globals]{Globals}{EndGlobals}{\textbf{Globals:\\}}{} 
+\algblockx[Assume]{Assumptions}{EndAssumptions}{\textbf{Assume:\\}}{} 
 
-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}.
 
+\chapter{Contribution} \label{chap:contribution}
 
-\section{W-DFS}
+The main theoretical contribution of this paper is an improvement on a
+$\max$-strategy improvement algorithm for solving fixpoint equations
+over the integers with monotonic
+operators\cite{Gawlitza:2007:PFC:1762174.1762203}. The original
+algorithm is presented in Section \ref{section:basic-algorithm}. We
+employ the ideas of Seidl, et al. to design an algorithm which runs in
+considerably less time than the existing solver.
+
+In this chapter we will begin by presenting the Work-list Depth First
+Search (W-DFS) fixpoint algorithm developed by Seidl, et
+al.\cite{DBLP:tr/trier/MI96-11}. We will then present a modification
+to the algorithm to allow it to perform $\max$-strategy iteration
+rather than fixpoint iteration. The chapter will then conclude with
+our Local Demand-driven Strategy Improvement (LDSI) algorithm.
+
+The existing algorithm as presented in Section
+\ref{section:basic-algorithm} consists of two iterative operations:
+fixpoint iteration and max-strategy iteration. Each of these
+operations consists of naively ``evaluating'' the system repeatedly
+until a further evaluation yields no change. It is shown by Gawlitza,
+et al. that these iterations must converge in a finite number of
+steps\cite{Gawlitza:2007:PFC:1762174.1762203}, but in practice this
+naive approach performs many more operations than are necessary, in
+many cases merely re-calculating results which are already known.
+
+By making use of some data-dependencies within the equation systems it
+is possible to reduce the amount of work that is to be done quite
+considerably.
+
+In order to aid our explanation of these algorithms we will now define
+a few terms and notations. All variables are taken from the set $X$
+and all values from the set $\D$.
+
+\begin{definition}
+  \textbf{Variable Assignments:} $X \to \D$. A function from a
+  variable to a value in our domain. An underlined value
+  (eg. $\underline{\infty}$) indicates a variable assignment mapping
+  everything to that value. Variable assignments may be combined with
+  $\oplus$ in the following way:
+  \begin{align*}
+    \rho \oplus \varrho = \left\{\begin{array}{lc}
+        \varrho(x) & x \in \mathsf{domain}(\varrho) \\
+        \rho(x) & \mbox{otherwise}
+      \end{array}\right.
+  \end{align*}
+\end{definition}
+
+\begin{definition}
+  \textbf{Expressions:} For the purposes of this discussion we will
+  consider expressions, $e \in E$, as $e : (X \to \D) \to \D$, a
+  mapping from a variable assignment to the expression's value in that
+  assignment.
+\end{definition}
+
+\begin{definition}
+  \textbf{Equation System:} $\{ x = e_x \mid x \in X, e_x \in E \}$. An
+  equation system can also be considered as a function $\varepsilon :
+  (X \to D) \to (X \to D)$; $\varepsilon[\rho](x) = e_x(\rho)$.
+\end{definition}
+
+\begin{definition}
+  \textbf{Dependencies:} A variable $x$ is said to \emph{depend on}
+  $y$ if a change to the value of $y$ induces a change in the value of
+  $x$.
+\end{definition}
+
+\section{Fixpoint Iteration}
+\subsection{Kleene Iteration}
+
+A simple approach to fixpoint iteration over monotonic equations is to
+simply iterate over the system repeatedly until a reevaluation results
+in no change to the values of any variables. This approach will always
+reach the least/greatest solution if there is one to be found, but it
+will often perform many more evaluations than are necessary. This
+algorithm is presented in Listing \ref{algo:kleene}.
 
-\subsection{Fixpoint Iteration}
+\begin{algorithm}
+  \begin{algorithmic}
+    \Assumptions
+      \begin{tabularx}{0.9\textwidth}{rX}
+        $\rho $:&$ X \to \D$, a variable assignment \\
+        $\varepsilon $:&$ (X \to \D) \to (X \to \D)$, an equation system
+      \end{tabularx}
+    \EndAssumptions
+
+    \State $n = 0$
+    \State $\rho_0 = \underline{\infty}$
+    \Repeat
+      \State $\rho_{n+1} = \varepsilon[ \rho_{n} ]$
+      \State $n = n + 1$
+    \Until {$\rho_{n-1} = \rho_n$}
+    \State \Return $\rho_n$
+  \end{algorithmic}
+  \caption{The Kleene iteration algorithm for solving fixpoint
+    equations for their greatest solutions.}
+  \label{algo:kleene}
+\end{algorithm}
 
-\newcommand\stable{\mathsf{stable}}
-\newcommand\eval{\mathsf{eval}}
-\newcommand\solve{\mathsf{solve}}
-\newcommand\system{\mathsf{system}}
-\algblockx[Globals]{Globals}{EndGlobals}{\textbf{Globals:\\}}{} 
+For each iteration the entire system is evaluated, irrespective of
+whether it could possibly have changed value. This results in a
+considerable inefficiency in practice and thus an approach which can
+evaluate smaller portions of the system in each iteration would be a
+sensible improvement.
+
+\subsection{W-DFS algorithm}
+
+The W-DFS algorithm presented by Seidl, et al. takes into account some
+form of data-dependencies as it solves the system. This gives it the
+ability to leave portions of the system unevaluated when it is certain
+that those values have not changed.
 
 \begin{algorithm}
   \begin{algorithmic}
     \Globals
-    \begin{tabular}{rl}
-      D & A mapping from variables to their current values, starting
+    \begin{tabularx}{0.9\textwidth}{rX}
+      $D : X \to \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}
+    \end{tabularx}
     \EndGlobals
+    something something
+  \end{algorithmic}
 
+  \begin{algorithmic}
     \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
+    \EndFunction 
+  \end{algorithmic}
 
+  \begin{algorithmic}
     \Function {solve} {$x$}
     \Comment{Solve a specific variable and place its value in $D$}
     \If {$x \not \in \stable$}
@@ -75,25 +174,14 @@ algorithm \ref{algo:w-dfs}.
   \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.
+\section{$\max$-strategy Iteration}
+\subsection{Naive approach}
+
+TODO: Explanation of the naive approach
 
-\subsection{Max-Strategy Iteration}
+\subsection{Adapted W-DFS algorithm}
 
 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
@@ -103,18 +191,18 @@ 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
+those parts of the strategy which have changed. Listing
 \ref{algo:w-dfs-max} presents this variation on W-DFS.
 
 \begin{algorithm}
   \begin{algorithmic}
     \Globals
-    \begin{tabular}{rl}
+    \begin{tabularx}{0.9\textwidth}{rX}
       $\sigma$ & A mapping from $\max$-expressions to their current
-      sub-expressions, starting by \\& mapping to the first
+      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 \\
+      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
@@ -122,7 +210,7 @@ those parts of the strategy which have changed. Algorithm
       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}
+    \end{tabularx}
     \EndGlobals
 
     \Function {eval} {$x$, $y$}
@@ -176,9 +264,9 @@ 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
+This algorithm is presented in two parts. Listing
 \ref{algo:combined-fixpoint} presents the fixpoint-iteration portion
-of the algorithm, while \ref{algo:combined-max} presents the
+of the algorithm, while Listing \ref{algo:combined-max} presents the
 $\max$-strategy portion.  The correctness of this new algorithm is
 argued in \ref{sec:combined-correctness}.
 
@@ -186,7 +274,7 @@ argued in \ref{sec:combined-correctness}.
 \begin{algorithm}
   \begin{algorithmic}
     \Globals
-    \begin{tabular}{rl}
+    \begin{tabularx}{0.9\textwidth}{rX}
       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
@@ -194,7 +282,7 @@ argued in \ref{sec:combined-correctness}.
       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}
+    \end{tabularx}
     \EndGlobals
 
     \Function {eval} {$x$, $y$}
@@ -246,7 +334,7 @@ argued in \ref{sec:combined-correctness}.
 \begin{algorithm}
   \begin{algorithmic}
     \Globals
-    \begin{tabular}{rl}
+    \begin{tabularx}{0.9\textwidth}{rX}
       $\sigma$ & A mapping from $\max$-expressions to their current
       sub-expressions, starting by \\& mapping to the first
       sub-expression \\
@@ -263,7 +351,7 @@ argued in \ref{sec:combined-correctness}.
       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}
+    \end{tabularx}
     \EndGlobals
 
     \Function {eval} {$x$, $y$}