diff options
Diffstat (limited to 'tex')
| -rw-r--r-- | tex/thesis/contribution/contribution.tex | 194 | ||||
| -rw-r--r-- | tex/thesis/thesis.tex | 17 |
2 files changed, 151 insertions, 60 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$} diff --git a/tex/thesis/thesis.tex b/tex/thesis/thesis.tex index 844e321..8f64c07 100644 --- a/tex/thesis/thesis.tex +++ b/tex/thesis/thesis.tex @@ -37,6 +37,7 @@ \usepackage{xcolor} \usepackage{xspace} \usepackage{stmaryrd,tikz} +\usepackage{tabularx} \usepackage{float} \floatstyle{boxed} @@ -44,6 +45,8 @@ \lstset{language={Python}, literate={<=}{$\le$}{1}}%, frame=tlrb} \usetikzlibrary{arrows} + +\newcommand\D{\mathbb{D}} \newcommand\R{\mathbb{R}} \newcommand\Z{\mathbb{Z}} \newcommand\CZ{\overline{\Z}} @@ -134,20 +137,20 @@ \renewcommand{\thepage}{\arabic{page}} \setupParagraphs -%\input{introduction/introduction.tex} -%\input{litreview/litreview.tex} +\input{introduction/introduction.tex} +\input{litreview/litreview.tex} \input{contribution/contribution.tex} -%\input{evaluation/evaluation.tex} -%\input{experiments/experiments.tex} -%\input{results/results.tex} -%\input{conclusion/conclusion.tex} +\input{evaluation/evaluation.tex} +\input{experiments/experiments.tex} +\input{results/results.tex} +\input{conclusion/conclusion.tex} %%%%%%%%%%%% % End % Bibliography -\bibliographystyle{abbrvnat}%style/mybibstyle} +\bibliographystyle{abbrvnat} %style/mybibstyle} { \setstretch{1.25} \cleardoublepage |