summaryrefslogtreecommitdiff
path: root/tex/thesis/contribution
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis/contribution')
-rw-r--r--tex/thesis/contribution/contribution.tex335
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}