From 18a747edd76918e2a1a4fb608b2d3923fcc535fa Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Tue, 16 Oct 2012 13:26:07 +1100 Subject: A quick fix to the solver. --- impl/Expression.hpp | 8 ++++++++ impl/VariableAssignment.hpp | 12 ++++++++++-- impl/gmon.out | Bin 78165 -> 76225 bytes impl/systems/gmon.out | Bin 79219 -> 75981 bytes impl/systems/test.eqns | 24 ++++++++++-------------- 5 files changed, 28 insertions(+), 16 deletions(-) diff --git a/impl/Expression.hpp b/impl/Expression.hpp index 00bc9cd..0d48d70 100644 --- a/impl/Expression.hpp +++ b/impl/Expression.hpp @@ -27,6 +27,10 @@ struct Expression { return NULL; } + virtual MaxExpression* toMaxExpression() { + return NULL; + } + virtual Domain eval(const VariableAssignment&) const = 0; virtual Domain eval(const VariableAssignment& rho, const MaxStrategy&) const { @@ -145,6 +149,10 @@ struct MaxExpression : public OperatorExpression { MaxExpression(const unsigned int& id, const Maximum& op, const std::vector*>& arguments) : OperatorExpression(op, arguments), _id(id) { } + MaxExpression* toMaxExpression() { + return this; + } + const MaxExpression* toMaxExpression() const { return this; } diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp index ae5efd7..a9247b5 100644 --- a/impl/VariableAssignment.hpp +++ b/impl/VariableAssignment.hpp @@ -38,8 +38,16 @@ struct DynamicVariableAssignment : public VariableAssignment { if (_stable.contains(x)) { _stable.remove(x); _values[x] = infinity(); - - solve(x); + + IdSet > infl = _influence[x]; + _influence[x].clear(); + for (typename IdSet >::iterator + it = infl.begin(), + ei = infl.end(); + it != ei; + ++it) { + invalidate(_system.variable(*it)); + } } } diff --git a/impl/gmon.out b/impl/gmon.out index aff812c..f33c245 100644 Binary files a/impl/gmon.out and b/impl/gmon.out differ diff --git a/impl/systems/gmon.out b/impl/systems/gmon.out index 3240978..b5abe0e 100644 Binary files a/impl/systems/gmon.out and b/impl/systems/gmon.out differ diff --git a/impl/systems/test.eqns b/impl/systems/test.eqns index fb23f1e..af18a57 100644 --- a/impl/systems/test.eqns +++ b/impl/systems/test.eqns @@ -1,16 +1,12 @@ i-4[0] = max(-inf, 0) -neg-i4[0] = max(-inf, 0) -neg-i1-pre = max(-inf, guard(add(min(neg-i4[0], inf), min(i-4[0], inf)), 0, neg-i4[0]), guard(add(min(neg-i2-pre, inf), min(i-2-pre, inf)), 0, neg-i2-pre)) -i-1-pre = max(-inf, guard(add(min(neg-i4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(neg-i2-pre, inf), min(i-2-pre, inf)), 0, i-2-pre)) -neg-i3-pre = max(-inf, guard(add(min(neg-i1-pre, inf), min(i-1-pre, 2)), 0, neg-i1-pre)) -i-3-pre = max(-inf, guard(add(min(neg-i1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre))) -neg-i0-pre = max(-inf, guard(add(min(neg-i1-pre, -3), min(i-1-pre, inf)), 0, min(-3, neg-i1-pre))) -i-0-pre = max(-inf, guard(add(min(neg-i1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre)) +negi-4[0] = max(-inf, 0) +negi-1-pre = max(-inf, guard(add(min(negi-4[0], inf), min(i-4[0], inf)), 0, negi-4[0]), guard(add(min(negi-2-pre, inf), min(i-2-pre, inf)), 0, negi-2-pre)) +i-1-pre = max(-inf, guard(add(min(negi-4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(negi-2-pre, inf), min(i-2-pre, inf)), 0, i-2-pre)) +negi-3-pre = max(-inf, guard(add(min(negi-1-pre, inf), min(i-1-pre, 2)), 0, negi-1-pre)) +i-3-pre = max(-inf, guard(add(min(negi-1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre))) +negi-0-pre = max(-inf, guard(add(min(negi-1-pre, -3), min(i-1-pre, inf)), 0, min(-3, negi-1-pre))) +i-0-pre = max(-inf, guard(add(min(negi-1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre)) i-3[0] = max(-inf, add(0, i-3-pre)) -neg-i3[0] = max(-inf, add(0, neg-i3-pre)) -neg-i2-pre = max(-inf, guard(add(min(neg-i3[0], inf), min(i-3[0], inf)), 0, neg-i3[0])) -i-2-pre = max(-inf, guard(add(min(neg-i3[0], inf), min(i-3[0], inf)), 0, i-3[0])) -x = max(-inf, 0) -y = max(-inf, x, z) -z = max(-inf, y) - +negi-3[0] = max(-inf, add(0, negi-3-pre)) +negi-2-pre = max(-inf, guard(add(min(negi-3[0], inf), min(i-3[0], inf)), 0, negi-3[0])) +i-2-pre = max(-inf, guard(add(min(negi-3[0], inf), min(i-3[0], inf)), 0, i-3[0])) -- cgit v1.2.3 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 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 From b172bf1d48d415ecfc62d81981f4c65ea54a3187 Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Wed, 17 Oct 2012 11:11:33 +1100 Subject: Get rid of extra files produced during LaTeX compilation. --- tex/thesis/Makefile | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tex/thesis/Makefile b/tex/thesis/Makefile index 1ccb5c4..8609c3a 100644 --- a/tex/thesis/Makefile +++ b/tex/thesis/Makefile @@ -3,7 +3,7 @@ PROJ = thesis .PHONY: all pdf wc clean -all: pdf +all: pdf clean pdf: pdflatex $(PROJ) @@ -26,4 +26,3 @@ clean: rm -f `find . -name '*.lot'` rm -f `find . -name '*.out'` rm -f `find . -name '*~'` - -- cgit v1.2.3 From 39bcfdc55a09e437482768903f6093ab1dd60a61 Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Wed, 17 Oct 2012 15:39:40 +1100 Subject: More work on the thesis itself. --- tex/thesis/contribution/contribution.tex | 194 ++++++++++++++++++++++--------- 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 -- cgit v1.2.3 From 86ca7448849aaaea6db34b1d2bcf8d99d7d7b12c Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Mon, 22 Oct 2012 14:44:57 +1100 Subject: Okay, the solver is now correct. It runs in two separate passes: - improve strategy (for all) - evaluate fixpoint Unfortunately this loses out on locality at the moment. I really want a local solver, so I'll have to see what I can do about that. --- .gitignore | 1 + impl/Complete.hpp | 6 ++- impl/Expression.hpp | 6 ++- impl/MaxStrategy.hpp | 89 ++++++++++++++++++++++++++++++++++++-------- impl/VariableAssignment.hpp | 47 +++++++++++++++++------ impl/gmon.out | Bin 76225 -> 0 bytes impl/main.cpp | 15 ++++++++ impl/systems/gmon.out | Bin 75981 -> 0 bytes impl/systems/test.eqns | 32 ++++++++++------ impl/test/7.eqns | 8 ++++ impl/test/7.soln | 8 ++++ 11 files changed, 171 insertions(+), 41 deletions(-) delete mode 100644 impl/gmon.out delete mode 100644 impl/systems/gmon.out create mode 100644 impl/test/7.eqns create mode 100644 impl/test/7.soln diff --git a/.gitignore b/.gitignore index 3b01757..93c639b 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ /impl/build/* /impl/parser/* +gmon.out diff --git a/impl/Complete.hpp b/impl/Complete.hpp index 8c5559a..e3ec15a 100644 --- a/impl/Complete.hpp +++ b/impl/Complete.hpp @@ -40,7 +40,11 @@ struct Complete { return Complete(- _value, _infinity); } Complete operator+(const Complete& other) const { - if (_infinity) { + if (_infinity && other._infinity) { + if (_value > 0 || other._value > 0) + return Complete(1, true); + return Complete(-1, true); + } else if (_infinity) { return *this; } else if (other._infinity) { return other; diff --git a/impl/Expression.hpp b/impl/Expression.hpp index 0d48d70..9c4ac9f 100644 --- a/impl/Expression.hpp +++ b/impl/Expression.hpp @@ -110,6 +110,10 @@ struct OperatorExpression : public Expression { return _operator.eval(argumentValues); } + std::vector*>& arguments() { + return _arguments; + } + const std::vector*>& arguments() const { return _arguments; } @@ -141,7 +145,7 @@ struct OperatorExpression : public Expression { private: const Operator& _operator; protected: - const std::vector*> _arguments; + std::vector*> _arguments; }; template diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp index 96aeef4..f4026dd 100644 --- a/impl/MaxStrategy.hpp +++ b/impl/MaxStrategy.hpp @@ -10,6 +10,9 @@ template struct MaxStrategy { virtual ~MaxStrategy() { } virtual unsigned int get(const MaxExpression& e) const = 0; + virtual unsigned int get(const MaxExpression& e) { + return const_cast(this)->get(e); + } }; unsigned int stack_depth = 1; @@ -38,20 +41,38 @@ struct DynamicMaxStrategy : public MaxStrategy { _influence(system.maxExpressionCount(), IdSet >(system.maxExpressionCount())), _var_influence(system.variableCount(), - IdSet >(system.maxExpressionCount())) + IdSet >(system.maxExpressionCount())), + _frozen(false) {} + void freeze() { + _frozen = true; + } + + void thaw() { + _frozen = false; + } + + bool is_frozen() { + return _frozen; + } + void setRho(DynamicVariableAssignment& rho) { _rho = ρ } unsigned int get(const MaxExpression& e) const { - solve(e); return _values[e]; } - void invalidate(const Variable& v) const { - log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; + unsigned int get(const MaxExpression& e) { + if (!_frozen) + solve(e); + return _values[e]; + } + + void invalidate(const Variable& v) { + log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; _stable.filter(_var_influence[v]); IdSet > infl = _var_influence[v]; @@ -67,7 +88,7 @@ struct DynamicMaxStrategy : public MaxStrategy { } private: - void solve(const MaxExpression& x) const { + void solve(const MaxExpression& x) { if (!_stable.contains(x)) { _stable.insert(x); log::strategy << indent() << "Stabilise " << x << std::endl; @@ -106,7 +127,7 @@ private: } struct DependencyAssignment : public VariableAssignment{ - DependencyAssignment(const DynamicMaxStrategy& strat, + DependencyAssignment(DynamicMaxStrategy& strat, VariableAssignment& rho, const MaxExpression& expr) : _strat(strat), @@ -118,13 +139,13 @@ private: return _rho[var]; } private: - const DynamicMaxStrategy& _strat; + DynamicMaxStrategy& _strat; VariableAssignment& _rho; const MaxExpression& _expr; }; struct DependencyStrategy : public MaxStrategy { - DependencyStrategy(const DynamicMaxStrategy& strat, const MaxExpression& expr) + DependencyStrategy(DynamicMaxStrategy& strat, const MaxExpression& expr) : _strat(strat), _expr(expr) { } @@ -136,19 +157,57 @@ private: return _strat._values[e]; } private: - const DynamicMaxStrategy& _strat; + DynamicMaxStrategy& _strat; const MaxExpression& _expr; }; -private: +private: const EquationSystem& _system; - mutable DynamicVariableAssignment* _rho; - mutable IdMap,unsigned int> _values; - mutable IdSet > _stable; - mutable IdMap,IdSet > > _influence; - mutable IdMap,IdSet > > _var_influence; + DynamicVariableAssignment* _rho; + IdMap,unsigned int> _values; + IdSet > _stable; + IdMap,IdSet > > _influence; + IdMap,IdSet > > _var_influence; + bool _frozen; }; + +template +IdMap,T> solve_for(const EquationSystem& system) { + IdMap,T> result(system.variableCount(), infinity()); + + DynamicMaxStrategy strategy(system); + DynamicVariableAssignment rho(system, strategy, -infinity()); + strategy.setRho(rho); + + bool changed; + do { + changed = false; + + // improve strategy + rho.freeze(); + strategy.thaw(); + for (unsigned int i = 0; i < system.variableCount(); ++i) { + strategy.get(*system[system.variable(i)]); + } + + // iterate fixpoint + strategy.freeze(); + rho.thaw(); + for (unsigned int i = 0; i < system.variableCount(); ++i) { + Variable& var = system.variable(i); + T val = rho[var]; + if (result[var] != val) { + result[var] = val; + changed = true; + } + } + } while(changed); + + return result; +} + + /*template std::ostream& operator<<(std::ostream& cout, const MaxStrategy& strat) { strat.print(cout); diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp index a9247b5..2a63756 100644 --- a/impl/VariableAssignment.hpp +++ b/impl/VariableAssignment.hpp @@ -8,6 +8,9 @@ template struct VariableAssignment { virtual ~VariableAssignment() { } virtual const Domain& operator[](const Variable&) const = 0; + virtual const Domain& operator[](const Variable& x) { + return (*const_cast(this))[x]; + } }; #include "EquationSystem.hpp" @@ -19,21 +22,40 @@ template struct DynamicVariableAssignment : public VariableAssignment { DynamicVariableAssignment( const EquationSystem& system, - const DynamicMaxStrategy& strat + DynamicMaxStrategy& strat, + const Domain& value=infinity() ) : _system(system), _strategy(strat), - _values(system.variableCount(), infinity()), + _values(system.variableCount(), value), _stable(system.variableCount()), _influence(system.variableCount(), - IdSet >(system.variableCount())) + IdSet >(system.variableCount())), + _frozen(false) { } + void freeze() { + _frozen = true; + } + + void thaw() { + _frozen = false; + } + + bool is_frozen() { + return _frozen; + } + const Domain& operator[](const Variable& var) const { - solve(var); return _values[var]; } - void invalidate(const Variable& x) const { + const Domain& operator[](const Variable& var) { + if (!_frozen) + solve(var); + return _values[var]; + } + + void invalidate(const Variable& x) { log::fixpoint << indent() << "Invalidating " << x << std::endl; if (_stable.contains(x)) { _stable.remove(x); @@ -53,7 +75,7 @@ struct DynamicVariableAssignment : public VariableAssignment { private: - void solve(const Variable& x) const { + void solve(const Variable& x) { if (!_stable.contains(x)) { _stable.insert(x); log::fixpoint << indent() << "Stabilise " << x << std::endl; @@ -90,7 +112,7 @@ private: } struct DependencyAssignment : public VariableAssignment { - DependencyAssignment(const DynamicVariableAssignment& assignment, const Variable& var) + DependencyAssignment(DynamicVariableAssignment& assignment, const Variable& var) : _assignment(assignment), _var(var) { } const Domain& operator[](const Variable& x) const { const Domain& result = _assignment[x]; @@ -98,15 +120,16 @@ private: return result; } private: - const DynamicVariableAssignment& _assignment; + DynamicVariableAssignment& _assignment; const Variable& _var; }; const EquationSystem& _system; - const DynamicMaxStrategy& _strategy; - mutable IdMap, Domain> _values; - mutable IdSet > _stable; - mutable IdMap,IdSet > > _influence; + DynamicMaxStrategy& _strategy; + IdMap, Domain> _values; + IdSet > _stable; + IdMap,IdSet > > _influence; + bool _frozen; }; #endif diff --git a/impl/gmon.out b/impl/gmon.out deleted file mode 100644 index f33c245..0000000 Binary files a/impl/gmon.out and /dev/null differ diff --git a/impl/main.cpp b/impl/main.cpp index e3e0ae3..84f17dd 100644 --- a/impl/main.cpp +++ b/impl/main.cpp @@ -140,6 +140,20 @@ int main (int argc, char* argv[]) { log::debug << system << endl; system.indexMaxExpressions(); // make reverse-lookup O(1) instead of O(n) + IdMap,ZBar> result = solve_for(system); + if (variables.size() > 0) { + for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { + Variable& var = system.variable(i); + if (variables.find(var.name()) != variables.end()) + cout << var.name() << " = " << result[var] << endl; + } + } else { + for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { + Variable& var = system.variable(i); + cout << var.name() << " = " << result[var] << endl; + } + } + /* DynamicMaxStrategy strategy(system); DynamicVariableAssignment rho(system, strategy); strategy.setRho(rho); @@ -156,6 +170,7 @@ int main (int argc, char* argv[]) { cout << var.name() << " = " << rho[var] << endl; } } + */ parser -> free(parser); tokens -> free(tokens); diff --git a/impl/systems/gmon.out b/impl/systems/gmon.out deleted file mode 100644 index b5abe0e..0000000 Binary files a/impl/systems/gmon.out and /dev/null differ diff --git a/impl/systems/test.eqns b/impl/systems/test.eqns index af18a57..a3b521d 100644 --- a/impl/systems/test.eqns +++ b/impl/systems/test.eqns @@ -1,12 +1,20 @@ -i-4[0] = max(-inf, 0) -negi-4[0] = max(-inf, 0) -negi-1-pre = max(-inf, guard(add(min(negi-4[0], inf), min(i-4[0], inf)), 0, negi-4[0]), guard(add(min(negi-2-pre, inf), min(i-2-pre, inf)), 0, negi-2-pre)) -i-1-pre = max(-inf, guard(add(min(negi-4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(negi-2-pre, inf), min(i-2-pre, inf)), 0, i-2-pre)) -negi-3-pre = max(-inf, guard(add(min(negi-1-pre, inf), min(i-1-pre, 2)), 0, negi-1-pre)) -i-3-pre = max(-inf, guard(add(min(negi-1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre))) -negi-0-pre = max(-inf, guard(add(min(negi-1-pre, -3), min(i-1-pre, inf)), 0, min(-3, negi-1-pre))) -i-0-pre = max(-inf, guard(add(min(negi-1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre)) -i-3[0] = max(-inf, add(0, i-3-pre)) -negi-3[0] = max(-inf, add(0, negi-3-pre)) -negi-2-pre = max(-inf, guard(add(min(negi-3[0], inf), min(i-3[0], inf)), 0, negi-3[0])) -i-2-pre = max(-inf, guard(add(min(negi-3[0], inf), min(i-3[0], inf)), 0, i-3[0])) +i-6[0] = max(-inf, 0) +neg-i-6[0] = max(-inf, 0) +neg-i-1-pre = max(-inf, guard(add(min(neg-i-6[0], inf), min(i-6[0], inf)), 0, neg-i-6[0]), guard(add(min(neg-i-2[0], inf), min(i-2[0], inf)), 0, neg-i-2[0])) +i-1-pre = max(-inf, guard(add(min(neg-i-6[0], inf), min(i-6[0], inf)), 0, i-6[0]), guard(add(min(neg-i-2[0], inf), min(i-2[0], inf)), 0, i-2[0])) +neg-i-5-pre = max(-inf, guard(add(min(neg-i-1-pre, inf), min(i-1-pre, 2)), 0, neg-i-1-pre)) +i-5-pre = max(-inf, guard(add(min(neg-i-1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre))) +neg-i-0-pre = max(-inf, guard(add(min(neg-i-1-pre, -3), min(i-1-pre, inf)), 0, min(-3, neg-i-1-pre))) +i-0-pre = max(-inf, guard(add(min(neg-i-1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre)) +neg-i-4-pre = max(-inf, guard(add(min(neg-i-5-pre, inf), min(i-5-pre, 1)), 0, neg-i-5-pre)) +i-4-pre = max(-inf, guard(add(min(neg-i-5-pre, inf), min(i-5-pre, 1)), 0, min(1, i-5-pre))) +neg-i-3-pre = max(-inf, guard(add(min(neg-i-5-pre, -2), min(i-5-pre, inf)), 0, min(-2, neg-i-5-pre))) +i-3-pre = max(-inf, guard(add(min(neg-i-5-pre, -2), min(i-5-pre, inf)), 0, i-5-pre)) +i-4[0] = max(-inf, add(1, i-4-pre)) +neg-i-4[0] = max(-inf, add(-1, neg-i-4-pre)) +neg-i-2-pre = max(-inf, guard(add(min(neg-i-4[0], inf), min(i-4[0], inf)), 0, neg-i-4[0]), guard(add(min(neg-i-3[0], inf), min(i-3[0], inf)), 0, neg-i-3[0])) +i-2-pre = max(-inf, guard(add(min(neg-i-4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(neg-i-3[0], inf), min(i-3[0], inf)), 0, i-3[0])) +i-3[0] = max(-inf, 10) +neg-i-3[0] = max(-inf, -10) +i-2[0] = max(-inf, add(1, i-2-pre)) +neg-i-2[0] = max(-inf, add(-1, neg-i-2-pre)) diff --git a/impl/test/7.eqns b/impl/test/7.eqns new file mode 100644 index 0000000..2789f0e --- /dev/null +++ b/impl/test/7.eqns @@ -0,0 +1,8 @@ +x = 0 +y = max(-inf, x, a) +a = b +b = c +c = d +d = e +e = f +f = y diff --git a/impl/test/7.soln b/impl/test/7.soln new file mode 100644 index 0000000..0d85468 --- /dev/null +++ b/impl/test/7.soln @@ -0,0 +1,8 @@ +x = 0 +y = 0 +a = 0 +b = 0 +c = 0 +d = 0 +e = 0 +f = 0 -- cgit v1.2.3 From 14c0c8bb717a668084cae8cd4b359ffd6fca73b0 Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Mon, 22 Oct 2012 14:55:54 +1100 Subject: Try fixing clang to work with the fixed solver. (This may not compile, for an annoying reason. I'll check in again soon with something better-er, or whatever.) --- .../Analyses/IntervalSolver/MaxStrategy.hpp | 99 +++++++++++++++++----- .../Analyses/IntervalSolver/VariableAssignment.hpp | 77 ++++++++++++----- clang/lib/Analysis/Interval.cpp | 42 +++------ 3 files changed, 147 insertions(+), 71 deletions(-) diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp index 57dcdeb..f4026dd 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp @@ -10,6 +10,9 @@ template struct MaxStrategy { virtual ~MaxStrategy() { } virtual unsigned int get(const MaxExpression& e) const = 0; + virtual unsigned int get(const MaxExpression& e) { + return const_cast(this)->get(e); + } }; unsigned int stack_depth = 1; @@ -38,20 +41,38 @@ struct DynamicMaxStrategy : public MaxStrategy { _influence(system.maxExpressionCount(), IdSet >(system.maxExpressionCount())), _var_influence(system.variableCount(), - IdSet >(system.maxExpressionCount())) + IdSet >(system.maxExpressionCount())), + _frozen(false) {} + void freeze() { + _frozen = true; + } + + void thaw() { + _frozen = false; + } + + bool is_frozen() { + return _frozen; + } + void setRho(DynamicVariableAssignment& rho) { _rho = ρ } unsigned int get(const MaxExpression& e) const { - solve(e); return _values[e]; } - void invalidate(const Variable& v) const { - solver_log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; + unsigned int get(const MaxExpression& e) { + if (!_frozen) + solve(e); + return _values[e]; + } + + void invalidate(const Variable& v) { + log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; _stable.filter(_var_influence[v]); IdSet > infl = _var_influence[v]; @@ -67,10 +88,10 @@ struct DynamicMaxStrategy : public MaxStrategy { } private: - void solve(const MaxExpression& x) const { + void solve(const MaxExpression& x) { if (!_stable.contains(x)) { _stable.insert(x); - solver_log::strategy << indent() << "Stabilise " << x << std::endl; + log::strategy << indent() << "Stabilise " << x << std::endl; stack_depth++; unsigned int val = x.bestStrategy(DependencyAssignment(*this, *_rho, x), @@ -78,7 +99,7 @@ private: stack_depth--; if (val != _values[x]) { - solver_log::strategy << x << " => " << *x.arguments()[val] << std::endl; + log::strategy << x << " => " << *x.arguments()[val] << std::endl; IdSet > oldInfluence = _influence[x]; _influence[x].clear(); @@ -96,15 +117,17 @@ private: solve(_system.maxExpression(*it)); } } else { - solver_log::strategy << indent() << x << " did not change" << std::endl; + log::strategy << indent() << x << " did not change: " + << x << " => " << *x.arguments()[val] << std::endl; } } else { - solver_log::strategy << indent() << x << " is stable" << std::endl; + log::strategy << indent() << x << " is stable: " + << x << " => " << *x.arguments()[_values[x]] << std::endl; } } struct DependencyAssignment : public VariableAssignment{ - DependencyAssignment(const DynamicMaxStrategy& strat, + DependencyAssignment(DynamicMaxStrategy& strat, VariableAssignment& rho, const MaxExpression& expr) : _strat(strat), @@ -116,13 +139,13 @@ private: return _rho[var]; } private: - const DynamicMaxStrategy& _strat; + DynamicMaxStrategy& _strat; VariableAssignment& _rho; const MaxExpression& _expr; }; struct DependencyStrategy : public MaxStrategy { - DependencyStrategy(const DynamicMaxStrategy& strat, const MaxExpression& expr) + DependencyStrategy(DynamicMaxStrategy& strat, const MaxExpression& expr) : _strat(strat), _expr(expr) { } @@ -134,19 +157,57 @@ private: return _strat._values[e]; } private: - const DynamicMaxStrategy& _strat; + DynamicMaxStrategy& _strat; const MaxExpression& _expr; }; -private: +private: const EquationSystem& _system; - mutable DynamicVariableAssignment* _rho; - mutable IdMap,unsigned int> _values; - mutable IdSet > _stable; - mutable IdMap,IdSet > > _influence; - mutable IdMap,IdSet > > _var_influence; + DynamicVariableAssignment* _rho; + IdMap,unsigned int> _values; + IdSet > _stable; + IdMap,IdSet > > _influence; + IdMap,IdSet > > _var_influence; + bool _frozen; }; + +template +IdMap,T> solve_for(const EquationSystem& system) { + IdMap,T> result(system.variableCount(), infinity()); + + DynamicMaxStrategy strategy(system); + DynamicVariableAssignment rho(system, strategy, -infinity()); + strategy.setRho(rho); + + bool changed; + do { + changed = false; + + // improve strategy + rho.freeze(); + strategy.thaw(); + for (unsigned int i = 0; i < system.variableCount(); ++i) { + strategy.get(*system[system.variable(i)]); + } + + // iterate fixpoint + strategy.freeze(); + rho.thaw(); + for (unsigned int i = 0; i < system.variableCount(); ++i) { + Variable& var = system.variable(i); + T val = rho[var]; + if (result[var] != val) { + result[var] = val; + changed = true; + } + } + } while(changed); + + return result; +} + + /*template std::ostream& operator<<(std::ostream& cout, const MaxStrategy& strat) { strat.print(cout); diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp index ba5f650..2a63756 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp @@ -8,6 +8,9 @@ template struct VariableAssignment { virtual ~VariableAssignment() { } virtual const Domain& operator[](const Variable&) const = 0; + virtual const Domain& operator[](const Variable& x) { + return (*const_cast(this))[x]; + } }; #include "EquationSystem.hpp" @@ -19,46 +22,71 @@ template struct DynamicVariableAssignment : public VariableAssignment { DynamicVariableAssignment( const EquationSystem& system, - const DynamicMaxStrategy& strat + DynamicMaxStrategy& strat, + const Domain& value=infinity() ) : _system(system), _strategy(strat), - _values(system.variableCount(), infinity()), + _values(system.variableCount(), value), _stable(system.variableCount()), _influence(system.variableCount(), - IdSet >(system.variableCount())) + IdSet >(system.variableCount())), + _frozen(false) { } + void freeze() { + _frozen = true; + } + + void thaw() { + _frozen = false; + } + + bool is_frozen() { + return _frozen; + } + const Domain& operator[](const Variable& var) const { - solve(var); return _values[var]; } - void invalidate(const Variable& x) const { - solver_log::fixpoint << indent() << "Invalidating " << x << std::endl; + const Domain& operator[](const Variable& var) { + if (!_frozen) + solve(var); + return _values[var]; + } + + void invalidate(const Variable& x) { + log::fixpoint << indent() << "Invalidating " << x << std::endl; if (_stable.contains(x)) { _stable.remove(x); _values[x] = infinity(); - - solve(x); + + IdSet > infl = _influence[x]; + _influence[x].clear(); + for (typename IdSet >::iterator + it = infl.begin(), + ei = infl.end(); + it != ei; + ++it) { + invalidate(_system.variable(*it)); + } } } private: - void solve(const Variable& x) const { + void solve(const Variable& x) { if (!_stable.contains(x)) { _stable.insert(x); - solver_log::fixpoint << indent() << "Stabilise " << x << std::endl; + log::fixpoint << indent() << "Stabilise " << x << std::endl; stack_depth++; - if (!_system[x]) - return; - Domain val = _system[x]->evalWithStrat(DependencyAssignment(*this, x), - _strategy); + Domain val = _system[x]->eval(DependencyAssignment(*this, x), + _strategy); stack_depth--; if (val != _values[x]) { - solver_log::fixpoint << x << " = " << val << std::endl; + log::fixpoint << x << " = " << val << std::endl; IdSet > oldInfluence = _influence[x]; _influence[x].clear(); @@ -74,15 +102,17 @@ private: solve(_system.variable(*it)); } } else { - solver_log::fixpoint << indent() << x << " did not change" << std::endl; + log::fixpoint << indent() << x << " did not change: " + << x << " = " << val << std::endl; } } else { - solver_log::fixpoint << indent() << x << " is stable" << std::endl; + log::fixpoint << indent() << x << " is stable: " + << x << " = " << _values[x] << std::endl; } } struct DependencyAssignment : public VariableAssignment { - DependencyAssignment(const DynamicVariableAssignment& assignment, const Variable& var) + DependencyAssignment(DynamicVariableAssignment& assignment, const Variable& var) : _assignment(assignment), _var(var) { } const Domain& operator[](const Variable& x) const { const Domain& result = _assignment[x]; @@ -90,15 +120,16 @@ private: return result; } private: - const DynamicVariableAssignment& _assignment; + DynamicVariableAssignment& _assignment; const Variable& _var; }; const EquationSystem& _system; - const DynamicMaxStrategy& _strategy; - mutable IdMap, Domain> _values; - mutable IdSet > _stable; - mutable IdMap,IdSet > > _influence; + DynamicMaxStrategy& _strategy; + IdMap, Domain> _values; + IdSet > _stable; + IdMap,IdSet > > _influence; + bool _frozen; }; #endif diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp index ac96107..d005048 100644 --- a/clang/lib/Analysis/Interval.cpp +++ b/clang/lib/Analysis/Interval.cpp @@ -702,40 +702,24 @@ void IntervalAnalysis::runOnAllBlocks() { } } - std::vector a; - - a.push_back(&system.constant(-infinity())); - a.push_back(&system.constant(0)); - system[system.variable("x")] = &system.maxExpression(a); - a.clear(); - - system.variable("y"); - - a.push_back(&system.variable("x")); - a.push_back(&system.variable("z")); - EqnExpr* minExpr = &system.expression(new Maximum(), a); - a.clear(); - - a.push_back(&system.constant(-infinity())); - a.push_back(minExpr); - system[system.variable("y")] = &system.maxExpression(a); - a.clear(); - - a.push_back(&system.constant(-infinity())); - a.push_back(&system.variable("y")); - system[system.variable("z")] = &system.maxExpression(a); - - llvm::errs() << toString(system) << "\n"; - system.indexMaxExpressions(); - DynamicMaxStrategy strategy(system); - DynamicVariableAssignment rho(system, strategy); - strategy.setRho(rho); + IdMap result = solve_for(system); for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { + EqnVar& var = system.variable(i); + cout << var.name() << " = " << result[var] << endl; + } + + /* + DynamicMaxStrategy strategy(system); + DynamicVariableAssignment rho(system, strategy); + strategy.setRho(rho); + + for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { EqnVar& var = system.variable(size - i - 1); llvm::errs() << toString(var.name()) << " = " << toString(rho[var]) << "\n"; - } + } + */ } -- cgit v1.2.3