summaryrefslogtreecommitdiff
path: root/tex/thesis/contribution
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis/contribution')
-rw-r--r--tex/thesis/contribution/contribution.tex194
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$}
generated by cgit v1.2.3 (git 2.46.2) at 2024-12-26 05:09:49 +0000