From 7c8f10b9f5c8f4c28cc1574b372431f0f714245d Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Tue, 16 Oct 2012 16:18:19 +1100 Subject: Doop doop doop. Some contribution writing stuff. --- tex/thesis/contribution/contribution.tex | 335 +++++++++++++++++++++++++++++++ tex/thesis/references.bib | 6 + tex/thesis/thesis.tex | 15 +- tex/thesis/usydthesis.cls | 3 +- 4 files changed, 351 insertions(+), 8 deletions(-) create mode 100644 tex/thesis/contribution/contribution.tex (limited to 'tex') 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} diff --git a/tex/thesis/references.bib b/tex/thesis/references.bib index d03c67a..e743703 100644 --- a/tex/thesis/references.bib +++ b/tex/thesis/references.bib @@ -134,4 +134,10 @@ publisher = {OCG}, OPTnote = {}, OPTannote = {} +} +@misc{fixpoint-slides, + author = {Helmut Seidl}, + title = {Lecture Slides in Program Optimisation}, + url = {http://www2.in.tum.de/~seidl/Courses/WS2011/Optimierung/all2011.pdf}, + year = {2011} } \ No newline at end of file diff --git a/tex/thesis/thesis.tex b/tex/thesis/thesis.tex index 6983d79..844e321 100644 --- a/tex/thesis/thesis.tex +++ b/tex/thesis/thesis.tex @@ -134,19 +134,20 @@ \renewcommand{\thepage}{\arabic{page}} \setupParagraphs -\input{introduction/introduction.tex} -\input{litreview/litreview.tex} -\input{evaluation/evaluation.tex} -\input{experiments/experiments.tex} -\input{results/results.tex} -\input{conclusion/conclusion.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} %%%%%%%%%%%% % End % Bibliography -\bibliographystyle{style/mybibstyle} +\bibliographystyle{abbrvnat}%style/mybibstyle} { \setstretch{1.25} \cleardoublepage diff --git a/tex/thesis/usydthesis.cls b/tex/thesis/usydthesis.cls index e18eb53..5b1a4d4 100644 --- a/tex/thesis/usydthesis.cls +++ b/tex/thesis/usydthesis.cls @@ -32,7 +32,8 @@ \usepackage{amssymb,amsmath} \newcommand{\theHalgorithm}{\arabic{algorithm}} \usepackage[ruled]{algorithm} -\usepackage{algorithmic} +\usepackage{algorithmicx} +\usepackage{algpseudocode} % Fancy footnotes \usepackage[stable]{style/footmisc} -- cgit v1.2.3