From e207a8fec1bae01068bdb3a27a2090a4af5f8cb2 Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Wed, 31 Oct 2012 00:50:29 +1100 Subject: Remove _var_influence and do some writeup _var_influence was really just duplicating data that was available elsewhere, so I got rid of it. I also did some writing about the algorithm and stuff for the thesis. --- tex/thesis/Makefile | 5 + tex/thesis/contribution/contribution.tex | 221 +++++++++++++++++++++---------- 2 files changed, 159 insertions(+), 67 deletions(-) (limited to 'tex/thesis') diff --git a/tex/thesis/Makefile b/tex/thesis/Makefile index 5022129..ee64d9e 100644 --- a/tex/thesis/Makefile +++ b/tex/thesis/Makefile @@ -11,6 +11,11 @@ pdf: clean pdflatex $(PROJ) pdflatex $(PROJ) +remote: + rsync -r * honours:honours/tex/thesis/ + ssh honours "cd honours/tex/thesis; make" + rsync honours:honours/tex/thesis/thesis.pdf . + wc: wc `find . -name "*.tex"` diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex index 7d12299..66d5b4a 100644 --- a/tex/thesis/contribution/contribution.tex +++ b/tex/thesis/contribution/contribution.tex @@ -134,7 +134,7 @@ $O(n^3)$ right-hand-sides, and thus an approach which can evaluate smaller portions of the system in each iteration would be a significant improvement. -\subsection{W-DFS algorithm} +\subsection{W-DFS algorithm} \ref{sec:wdfs} 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 @@ -255,7 +255,7 @@ problem it is possible \end{algorithm} -\subsection{Adapted W-DFS algorithm} +\subsection{Adapted W-DFS algorithm} \ref{sec:adapted-wdfs} This, then, allows us to use the W-DFS algorithm to re-evaluate only those parts of the strategy which have changed. Listing @@ -327,17 +327,26 @@ be evaluated. The new \emph{Local Demand-driven Strategy Improvement} algorithm, \emph{LDSI}, seeks to do this. By adding an ``invalidate'' function to both W-DFS instances we provide an interface for the two -sides of the algorithm to indicate which values have changed. The -fixpoint-iteration operation can then be provided with a ``stabilise'' -function to solve a partially-unstable system. +sides of the algorithm to indicate which values have changed and +``destabilise'' that portion of the system. This essentially results in a $\max$-strategy iteration which, at each strategy-improvement step, invalidates a portion of the current -fixpoint iteration. The fixpoint iteration then re-stabilises itself -by evaluating what values have been changed before returning control -to the $\max$-strategy iteration to change the system again. The back -and forth continues in this way until the $\max$-strategy can not -improve the strategy any further. +fixpoint iteration which may depend on the changed strategy. The +fixpoint iteration then re-stabilises itself by evaluating what values +have been changed, but only when such values are requested by the +$\max$-strategy iteration. The $\max$-strategy can continue as normal, +invalidating the fixpoint-iteration as required, and simply assume +that the fixpoint-iteration will provide it with the correct values +from the greatest fixpoint. + + +This entire approach is demand driven, and so any necessary evaluation +is delayed until the point when it is actually required. Additionally, +if it is not necessary to evaluate a particular right hand side in +order to make a decision then the algorithm will attempt to avoid +evaluating it. + @@ -356,23 +365,23 @@ correctness of this new algorithm is argued in \begin{algorithmic} \Globals \begin{tabularx}{0.9\textwidth}{rX} - $V$ & $\{X \to \D\}$ - a mapping from variables to values, + $D$ & $X \to \D$ - a mapping from variables to values, starting at $\{ x \mapsto \infty \}$ \\ - $I_{X,X}$ & $\{X \to X\}$ - a mapping from a variable to the + $\sigma$ & $E_{\max} \to E$ - a mapping from $\max$-expressions + to their sub-expressions (a $\max$-strategy) \\ + + $I_{X,X}$ & $X \to X$ - a mapping from a variable to the variables it influences \\ - $I_{\max,\max}$ & $\{E_{\max} \to E_{\max}\}$ - a mapping from a + $I_{\max,\max}$ & $E_{\max} \to E_{\max}$ - a mapping from a $\max$-expression to the $\max$-expressions it influences \\ - $I_{X,\max}$ & $\{X \to E_{\max}\}$ - a mapping from a variable - to the $\max$-expressions it influences \\ - $U_{X}$ & The set of all variables whose values have not stabilised to a final fixpoint value (unstable variables) \\ - $U_{\max}$ & The set of all $\max$ expressions whose strategies - have not yet stabilised to their final strategy (unstable + $S_{\max}$ & The set of all $\max$ expressions whose strategies + have stabilised to their final strategy (stable $\max$-expressions) \\ $\varepsilon$ & The equation system, a mapping from a variable @@ -384,12 +393,27 @@ correctness of this new algorithm is argued in \label{algo:ldsi:fixpoint:globals} \end{algorithm} +A few things are of particular note for the global variables. In +particular the difference between $U_X$ being an unstable set and +$S_{\max}$ being a stable set. In reality these two are entirely +equivalent, but because the fixpoint-iteration will be started as +being entirely ``stable'' (with values of $-\infty$) it is of more +practical benefit to avoid the extra work populating the ``stable'' +set by instead storing unstable values. + +The other variables are just the state from each of the previous +algorithms for intelligently performing $\max$-strategy iteration and +fixpoint iteration (as were presented in Sections \ref{sec:wdfs} +and \ref{sec:adapted-wdfs}). $D$ and $I_{X,X}$ are taken from the +W-DFS algorithm, while $\sigma$ and $I_{\max,\max}$ are taken from the +Adapted W-DFS algorithm. + \begin{algorithm}[H] \begin{algorithmic} - \Function {evalfixpoint} {$x$, $y$} + \Function {evalfixpoint} {$x \in X$, $y \in X$} \State $\solve \fixpoint(y)$ \State $I_{X,X}[y] = I_{X,X}[y] \cup \{x\}$ \State \Return $D[y]$ @@ -399,9 +423,17 @@ correctness of this new algorithm is argued in \label{algo:ldsi:fixpoint:eval} \end{algorithm} +This procedure is exactly the same as the equivalent method in the +W-DFS algorithm. It allows us to more easily track dependencies +between fixpoint variables by injecting this function as our +variable-lookup function. It then both calculates a new value for the +variable (the $\solve \fixpoint$ call) and notes the dependency +between $x$ and $y$. + \begin{algorithm}[H] \begin{algorithmic} - \Function {invalidatefixpoint} {$x$} + \Function {invalidatefixpoint} {$x \in X$} + \Comment{Invalidate a fixpoint variable} \If {$x \not \in U_X$} \State $U_X = U_X \cup \{x\}$ \State $D[x] = \infty$ @@ -418,6 +450,16 @@ correctness of this new algorithm is argued in \label{algo:ldsi:fixpoint:invalidate} \end{algorithm} +This procedure is not called in the fixpoint iteration process, but is +rather the method by which the $\max$-strategy iteration can +communicate with the fixpoint-iteration. It allows the $\max$-strategy +iteration to inform the fixpoint-iteration which values have changed +and will require re-evaluation. This makes it possible to only +re-evaluate a partial system (the solving of which is also be delayed +until requested by the $\solve \fixpoint$ procedure). + + + \begin{algorithm}[H] \begin{algorithmic} \Function {solvefixpoint} {$x$} @@ -425,7 +467,7 @@ correctness of this new algorithm is argued in \If {$x \in U_X$} \State $f = \system[x]$ \State $U_X = U_X \backslash \{x\}$ - \State $v = f( \lambda y . \eval(x, y) )$ + \State $v = \sigma(\system[x])( \lambda y . \eval \fixpoint(x, y) )$ \If {$v \ne D[x]$} \State $D = \{ x \mapsto v \} \oplus D$ \State $W = I_{X,X}[x]$ @@ -446,62 +488,110 @@ correctness of this new algorithm is argued in After an evaluation of the $\solve \fixpoint$ procedure, the variable supplied as its argument will have been stabilised within the current -$\max$-strategy. +$\max$-strategy. This means that it will have taken on the same value +as it would take in the greatest fixpoint of this system. Because the +$\solve \fixpoint$ calls need not be made immediately it's possible +for a variable to be invalidated by several $\max$-strategy +improvements without being re-evaluated. + -After an evaluation of the $\stabilise \fixpoint$ procedure all -currently ``unstable'' variables in the current fixpoint will be -solved. This correlates to performing an entire fixpoint-iteration for -the greatest-fixpoint of the unstable portion of the equation -system. This is meant to be used to perform a sufficient -fixpoint-iteration to allow for the next $\max$-strategy improvement -step, but this relies on the $\max$-strategy solver to correctly -invalidate the fixpoint-iteration portion of the algorithm. \begin{algorithm}[H] \begin{algorithmic} - \Function {evalstrategy} {$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\}$ + \Function {evalstrategy} {$x \in E_{\max}$, $y \in E_{\max}$} + \Comment{Evaluate $y$ for its value and note that when $y$ + changes, $x$ must be re-evaluated} + \State $\solve \strategy(y)$ + \State $I_{\max,\max}[y] = I_{\max,\max}[y] \cup \{x\}$ \State \Return $\sigma[y]$ \EndFunction + \Function {evalstrategyfixpoint} {$x \in E_{\max}$, $y \in X$} + \Comment{Evaluate $y$ for its value and note that when $y$ + changes, $x$ must be re-evaluated} + \State $\solve \fixpoint(y)$ + \State $I_{\max,\max}[y] = I_{\max,\max}[\system[y]] \cup \{x\}$ + \State \Return $D[y]$ + \EndFunction + \end{algorithmic} + \label{algo:ldsi:strategy:eval} + \caption{Evaluate a portion of the $\max$-strategy and note a + dependency} +\end{algorithm} + +The $\eval \strategy$ function is essentially the same as the $\eval +\fixpoint$ function, except that it notes the dependencies in a +different variable, $I_{\max,\max}$. This is because the dependency +information for the $\max$-strategy iteration is entirely separate to +that of the fixpoint iteration. + +The $\solve \fixpoint$ calls in $\eval \strategy \fixpoint$ are +top-level calls, meaning that upon their return we know that $D$ +contains the value it would take in the greatest fixpoint of the +current strategy $\sigma$. This function, therefore, acts as a simple +intermediate layer between the fixpoint-iteration and the +$\max$-strategy iteration to allow for dependencies to be tracked. + +\begin{algorithm}[H] + \begin{algorithmic} \Function {invalidatestrategy} {$x \in X$} \Comment{$x$ is a \emph{variable}} - \If {$x \not \in U_X$} - \State $U_X = U_X \cup \{x\}$ - \State $W = I[x]$ - \State $I[x] = \emptyset$ - \For {$v \in W$} - \State $\invalidate \fixpoint(v)$ + \For {$v \in I_{\max,\max}(\system[x])$} \Comment{$v$ is + influenced by $x$} + \State $\invalidate \strategy (v)$ + \EndFor + \EndFunction + + \Function {invalidatestrategy} {$x \in E_{\max}$} \Comment{$x$ is + a \emph{$\max$-expression}} + \If {$x \in S_{\max}$} + \State $S_{\max} = S_{\max} \backslash \{x\}$ + \For {$v \in I_{\max,\max}$} \Comment {$v$ is influenced by $x$} + \State $\invalidate \strategy (v)$ \EndFor \EndIf \EndFunction + \end{algorithmic} + \label{algo:ldsi:strategy:invalidate} + \caption{Evaluate a portion of the $\max$-strategy and note a + dependency} +\end{algorithm} + +Invalidating the $\max$-strategy iteration is slightly more +complicated than invalidating the fixpoint iteration stage. As the +invalidation interface consists of variables, we must first translate +a variable into a $\max$-expression (which is easily done by looking +it up in the equation system). We must then invalidate the strategies +for each variable which depends on this resultant +$\max$-expression. The invalidation for $\max$-expressions consists of +transitively invalidating everything which depends on the +$\max$-expression, as well as itself. + + - \Function {solvestrategy} {$x$} +\begin{algorithm}[H] + \begin{algorithmic} + \Function {solvestrategy} {$x \in E_{\max}$} \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(f, \sigma(), \lambda y . \eval(x, y))$ - \If {$v \ne \sigma[x]$} - \State $\sigma = \{ x \mapsto v \} \oplus \sigma$ - \State $W = I[x]$ - \State $I(x) = \emptyset$ - \State $\invalidate \fixpoint(\mathsf{lookupVarFor}(x))$ - \State $\stable = \stable \backslash W$ - \For {$v \in W$} + \If {$x \not \in S_{\max}$} + \State $S_{\max} = S_{\max} \cup \{x\}$ + \State $\sigma_{dynamic} = \lambda y . \eval \strategy(x,y)$ + \State $e = P_{\max}(\sigma_{dynamic}, + \lambda y . \eval \strategy \fixpoint(x, y))(x)$ + \If {$e \ne \sigma[x]$} + \State $\sigma = \{ x \mapsto e \} \oplus \sigma$ + \State $\invalidate \fixpoint(\system^{-1}(x))$ + \State $S_{\max} = S_{\max} \backslash I[x]$ + \For {$v \in I[x]$} \State $\solve(v)$ \EndFor \EndIf \EndIf \EndFunction \end{algorithmic} - \caption{The $\max$-strategy portion of the Combined W-DFS.} - \label{algo:combined-max} + \label{algo:ldsi:solve} \end{algorithm} @@ -516,15 +606,12 @@ 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} +The fixpoint iteration step invalidates anything that \emph{might} +depend on $x$ while it invalidates $x$, thereby ensuring that any +further calls to $\solve \fixpoint$ will result in a correct value for +the given strategy. + +The strategy-iteration step invalidates anything that \emph{might} +depend on $\system[x]$ while it invalidates $x$, thereby ensuring that +any further calls to $\solve \strategy$ will result in a correct value +for the given strategy. -- cgit v1.2.3 From 4a9538d5bb324add6ebd818312e88045b868f944 Mon Sep 17 00:00:00 2001 From: Thomas Martin Gawlitza Date: Wed, 31 Oct 2012 15:08:48 +0100 Subject: . --- tex/thesis/thesis.tex | 2 ++ 1 file changed, 2 insertions(+) (limited to 'tex/thesis') diff --git a/tex/thesis/thesis.tex b/tex/thesis/thesis.tex index 8f64c07..2397833 100644 --- a/tex/thesis/thesis.tex +++ b/tex/thesis/thesis.tex @@ -91,6 +91,8 @@ \begin{document} +\allowdisplaybreaks + % initial page numbers: i, ii, iii, ... \renewcommand{\thepage}{\roman{page}} -- cgit v1.2.3 From b7eaa99578037789a337c5061c0ea8ee3150b63c Mon Sep 17 00:00:00 2001 From: "Zancanaro; Carlo" Date: Thu, 1 Nov 2012 18:06:13 +1100 Subject: A bunch of fixes to the solver, and moving it in to clang. Also some contribution writing stuff. Basically: lots of work. --- .../Analysis/Analyses/IntervalSolver/Complete.hpp | 7 +- .../Analyses/IntervalSolver/EquationSystem.hpp | 12 +- .../Analyses/IntervalSolver/Expression.hpp | 82 +++++++++--- .../Analysis/Analyses/IntervalSolver/IdMap.hpp | 13 +- .../Analysis/Analyses/IntervalSolver/IdSet.hpp | 4 + .../clang/Analysis/Analyses/IntervalSolver/Log.hpp | 18 +-- .../Analyses/IntervalSolver/MaxStrategy.hpp | 146 ++++++++++++++++----- .../Analysis/Analyses/IntervalSolver/Operator.hpp | 11 +- .../Analyses/IntervalSolver/VariableAssignment.hpp | 83 +++++++----- clang/lib/Analysis/Interval.cpp | 35 +---- impl/Expression.hpp | 3 +- impl/MaxStrategy.hpp | 55 +++----- impl/VariableAssignment.hpp | 7 - impl/main.cpp | 3 +- impl/systems/test.eqns | 24 ++-- impl/test/1.eqns | 2 +- impl/test/10.soln | 10 +- impl/test/7.soln | 4 +- impl/test/8.soln | 2 +- impl/test/9.soln | 4 +- impl/test/run | 6 +- tex/thesis/contribution/contribution.tex | 30 ++++- 22 files changed, 330 insertions(+), 231 deletions(-) (limited to 'tex/thesis') diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp index 9acb9d0..e3ec15a 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp @@ -1,6 +1,7 @@ #ifndef COMPLETE_HPP #define COMPLETE_HPP +#include #include #include @@ -39,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/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp index d95366d..3342cc7 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp @@ -91,13 +91,12 @@ struct EquationSystem { void indexMaxExpressions() { _expr_to_var = new IdMap,Variable*>(maxExpressionCount(), NULL); for (unsigned int i = 0, length = _right_sides.size(); i < length; ++i) { - if (_right_sides[i]) - _right_sides[i]->mapTo(*_variables[i], *_expr_to_var); + _right_sides[i]->mapTo(*_variables[i], *_expr_to_var); } } Variable* varFromExpr(const Expression& expr) const { - assert(_expr_to_var != NULL); // ensure we've indexed + assert(_expr_to_var); // make sure we've indexed const MaxExpression* maxExpr = expr.toMaxExpression();//dynamic_cast*>(&expr); if (maxExpr) { return (*_expr_to_var)[*maxExpr]; @@ -106,7 +105,7 @@ struct EquationSystem { } } - virtual bool equalAssignments(const VariableAssignment& l, const VariableAssignment& r) const { + virtual bool equalAssignments(VariableAssignment& l, VariableAssignment& r) const { for (unsigned int i = 0, length = _variables.size(); i < length; ++i) { @@ -121,10 +120,7 @@ struct EquationSystem { for (unsigned int i = 0, length = _variables.size(); i < length; ++i) { - if (_right_sides[i]) - cout << *_variables[i] << " = " << *_right_sides[i] << std::endl; - else - cout << *_variables[i] << " = NULL" << std::endl; + cout << *_variables[i] << " = " << *_right_sides[i] << std::endl; } } diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp index ac9b052..b59c7a2 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp @@ -4,6 +4,7 @@ #include #include #include +#include #include "IdMap.hpp" #include "Operator.hpp" @@ -27,15 +28,26 @@ struct Expression { return NULL; } - virtual Domain eval(const VariableAssignment&) const = 0; - virtual Domain evalWithStrat(const VariableAssignment& rho, + virtual MaxExpression* toMaxExpression() { + return NULL; + } + + virtual Domain eval(VariableAssignment&) const = 0; + virtual Domain eval(VariableAssignment& rho, const MaxStrategy&) const { return eval(rho); } + virtual Domain eval(VariableAssignment& rho, + MaxStrategy&) const { + return eval(rho); + } virtual void mapTo(Variable&, IdMap, Variable*>&) const { } + virtual void subMaxExprs(std::set*>&) const { + } + virtual void print(std::ostream&) const = 0; }; @@ -44,7 +56,7 @@ struct Constant : public Expression { Constant(const Domain& value) : _value(value) { } - virtual Domain eval(const VariableAssignment&) const { + virtual Domain eval(VariableAssignment&) const { return _value; } @@ -68,7 +80,7 @@ struct Variable : public Expression { return _name; } - virtual Domain eval(const VariableAssignment& rho) const { + virtual Domain eval(VariableAssignment& rho) const { return rho[*this]; } @@ -84,11 +96,9 @@ struct Variable : public Expression { template struct OperatorExpression : public Expression { OperatorExpression(const Operator& op, const std::vector*>& arguments) - : _operator(op), _arguments(arguments) { - assert(!arguments.empty()); - } + : _operator(op), _arguments(arguments) { } - virtual Domain eval(const VariableAssignment& rho) const { + virtual Domain eval(VariableAssignment& rho) const { std::vector argumentValues; for (typename std::vector*>::const_iterator it = _arguments.begin(); it != _arguments.end(); @@ -98,12 +108,22 @@ struct OperatorExpression : public Expression { return _operator.eval(argumentValues); } - virtual Domain evalWithStrat(const VariableAssignment& rho, const MaxStrategy& strat) const { + virtual Domain eval(VariableAssignment& rho, const MaxStrategy& strat) const { + std::vector argumentValues; + for (typename std::vector*>::const_iterator it = _arguments.begin(); + it != _arguments.end(); + ++it) { + argumentValues.push_back((*it)->eval(rho, strat)); + } + return _operator.eval(argumentValues); + } + + virtual Domain eval(VariableAssignment& rho, MaxStrategy& strat) const { std::vector argumentValues; for (typename std::vector*>::const_iterator it = _arguments.begin(); it != _arguments.end(); ++it) { - argumentValues.push_back((*it)->evalWithStrat(rho, strat)); + argumentValues.push_back((*it)->eval(rho, strat)); } return _operator.eval(argumentValues); } @@ -128,6 +148,14 @@ struct OperatorExpression : public Expression { } } + virtual void subMaxExprs(std::set*>& exprs) const { + for (unsigned int i = 0, length = _arguments.size(); + i < length; + ++i) { + _arguments[i]->subMaxExprs(exprs); + } + } + void print(std::ostream& cout) const { cout << _operator << "("; for (unsigned int i = 0, length = _arguments.size(); @@ -151,31 +179,40 @@ 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; } - virtual Domain evalWithStrat(const VariableAssignment& rho, const MaxStrategy& strat) const { - return this->_arguments[strat.get(*this)]->evalWithStrat(rho, strat); + virtual Domain eval(VariableAssignment& rho, const MaxStrategy& strat) const { + solver_log::fixpoint << "const MaxExpression eval" << std::endl; + return this->_arguments[strat.get(*this)]->eval(rho, strat); + } + + virtual Domain eval(VariableAssignment& rho, MaxStrategy& strat) const { + solver_log::strategy << "const MaxExpression eval" << std::endl; + return this->_arguments[strat.get(*this)]->eval(rho, strat); } - unsigned int bestStrategy(const VariableAssignment& rho, const MaxStrategy& strat) const { - Domain bestValue = this->evalWithStrat(rho, strat); - unsigned int bestIndex = strat.get(*this); + unsigned int bestStrategy(VariableAssignment& rho, MaxStrategy& strat, unsigned int bestIndex) const { + Domain bestValue = this->_arguments[bestIndex]->eval(rho, strat); for (unsigned int i = 0, length = this->_arguments.size(); i < length; ++i) { - const Domain value = this->_arguments[i]->evalWithStrat(rho, strat); + const Domain value = this->_arguments[i]->eval(rho, strat); if (bestValue < value) { - bestValue = value; bestIndex = i; + bestValue = value; } } return bestIndex; } - virtual void mapTo(Variable& v, IdMap, Variable*>& m) const { + virtual void mapTo(Variable& v, IdMap,Variable*>& m) const { m[*this] = &v; for (unsigned int i = 0, length = this->_arguments.size(); i < length; @@ -184,6 +221,15 @@ struct MaxExpression : public OperatorExpression { } } + virtual void subMaxExprs(std::set*>& exprs) const { + exprs.insert(this); + for (unsigned int i = 0, length = this->_arguments.size(); + i < length; + ++i) { + this->_arguments[i]->subMaxExprs(exprs); + } + } + unsigned int id() const { return _id; } diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp index 5e3aa3b..8cb25f8 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp @@ -1,13 +1,14 @@ #ifndef ID_MAP_HPP #define ID_MAP_HPP +#include #include template struct IdMap { IdMap(unsigned int length, V initial) : _length(length), _assignment(new V[length]) { - for (unsigned int i = 0; i < length; ++i) { + for (unsigned int i = 0; i < _length; ++i) { _assignment[i] = initial; } } @@ -32,17 +33,11 @@ struct IdMap { return *this; } virtual const V& operator[] (const T& x) const { - if (x.id() >= _length) { - std::cout << "throw exception" << *(char*)NULL; - //throw "Array out of bounds"; - } + assert(x.id() < _length); return _assignment[x.id()]; } virtual V& operator[] (const T& x) { - if (x.id() >= _length) { - std::cout << "throw exception" << *(char*)NULL; - //throw "Array out of bounds"; - } + assert(x.id() < _length); return _assignment[x.id()]; } diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/IdSet.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/IdSet.hpp index 950b1e1..bf98502 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/IdSet.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/IdSet.hpp @@ -96,6 +96,10 @@ class IdSet { return _set.size(); } + bool empty() const { + return _set.empty(); + } + private: unsigned int _range; std::set _set; diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Log.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Log.hpp index f9af7f2..90ab7e5 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Log.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Log.hpp @@ -1,26 +1,20 @@ #ifndef LOG_HPP #define LOG_HPP +// could not be hackier, but C++ is annoying +#define protected public +#include +#undef protected + #include #include #include #include namespace solver_log { - struct Logger : public std::ostream { - Logger(std::streambuf*, const std::string&) + Logger(std::streambuf* buffer, const std::string& name) : std::ostream(NULL) { } - - bool enabled() const { - return false; - } - - bool enabled(bool) { - return false; - } - - private: }; Logger strategy(std::cerr.rdbuf(), "strategy"); diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp index 57dcdeb..9ae7394 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp @@ -9,6 +9,9 @@ template struct MaxStrategy { virtual ~MaxStrategy() { } + virtual unsigned int get(const MaxExpression& e) { + return const_cast*>(this)->get(e); + } virtual unsigned int get(const MaxExpression& e) const = 0; }; @@ -37,54 +40,85 @@ struct DynamicMaxStrategy : public MaxStrategy { _stable(system.maxExpressionCount()), _influence(system.maxExpressionCount(), IdSet >(system.maxExpressionCount())), - _var_influence(system.variableCount(), - IdSet >(system.maxExpressionCount())) + _changed(false) {} void setRho(DynamicVariableAssignment& rho) { _rho = ρ } + void hasChanged(bool c) { + _changed = c; + } + + bool hasChanged() const { + return _changed; + } + unsigned int get(const MaxExpression& e) const { - solve(e); + solver_log::strategy << indent() << "Look up " << e << std::endl; return _values[e]; } - void invalidate(const Variable& v) const { - solver_log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; - _stable.filter(_var_influence[v]); + unsigned int get(const MaxExpression& e) { + solver_log::strategy << indent() << "Solve for " << e << std::endl; + solve(e); + return _values[e]; + } - IdSet > infl = _var_influence[v]; - _var_influence[v].clear(); + void invalidate(const Variable& v) { + solver_log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; + IdSet > infl = _influence[*_system[v]]; for (typename IdSet >::iterator it = infl.begin(), end = infl.end(); it != end; ++it) { - solve(_system.maxExpression(*it)); + invalidate(_system.maxExpression(*it)); + } + } + + void invalidate(const MaxExpression& v) { + if (_stable.contains(v)) { + solver_log::strategy << indent() << "Invalidating " << v << std::endl; + //solver_log::debug << indent() << " influence sets " << _influence << std::endl; + _stable.remove(v); + + IdSet > infl = _influence[v]; + for (typename IdSet >::iterator + it = infl.begin(), + end = infl.end(); + it != end; + ++it) { + invalidate(_system.maxExpression(*it)); + } } } 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; - stack_depth++; - unsigned int val = x.bestStrategy(DependencyAssignment(*this, *_rho, x), - DependencyStrategy(*this, x)); + stack_depth++; + DependencyAssignment assignment(*this, *_rho, x); + DependencyStrategy depStrat(*this, x); + unsigned int val = x.bestStrategy(assignment, depStrat, _values[x]); stack_depth--; if (val != _values[x]) { solver_log::strategy << x << " => " << *x.arguments()[val] << std::endl; IdSet > oldInfluence = _influence[x]; - _influence[x].clear(); + //_influence[x].clear(); _values[x] = val; + _changed = true; _rho->invalidate(*_system.varFromExpr(x)); + + //_rho->stabilise(); _stable.filter(oldInfluence); @@ -96,57 +130,107 @@ private: solve(_system.maxExpression(*it)); } } else { - solver_log::strategy << indent() << x << " did not change" << std::endl; + solver_log::strategy << indent() << x << " did not change: " + << x << " => " << *x.arguments()[val] << std::endl; } } else { - solver_log::strategy << indent() << x << " is stable" << std::endl; + solver_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), _rho(rho), - _expr(expr) { + _expr(expr), + _current(strat._system.variableCount()) { } - const Domain& operator[](const Variable& var) const { - _strat._var_influence[var].insert(_expr); + const Domain operator[](const Variable& var) { + // solve the strategy for this variable, too + _strat.solve(*_strat._system[var]); + _strat._influence[*_strat._system[var]].insert(_expr); return _rho[var]; } private: - const DynamicMaxStrategy& _strat; + DynamicMaxStrategy& _strat; VariableAssignment& _rho; const MaxExpression& _expr; + IdSet > _current; }; struct DependencyStrategy : public MaxStrategy { - DependencyStrategy(const DynamicMaxStrategy& strat, const MaxExpression& expr) + DependencyStrategy(DynamicMaxStrategy& strat, const MaxExpression& expr) : _strat(strat), _expr(expr) { } unsigned int get(const MaxExpression& e) const { + _strat._influence[e].insert(_expr); + return _strat._values[e]; + } + unsigned int get(const MaxExpression& e) { _strat.solve(e); - if (&_expr != &e) { - _strat._influence[e].insert(_expr); - } + _strat._influence[e].insert(_expr); return _strat._values[e]; } private: - const DynamicMaxStrategy& _strat; + DynamicMaxStrategy& _strat; const MaxExpression& _expr; }; +private: + const EquationSystem& _system; + DynamicVariableAssignment* _rho; + IdMap,unsigned int> _values; + IdSet > _stable; + IdMap,IdSet > > _influence; + bool _changed; +}; + + +template +struct Solver { + Solver(const EquationSystem& system) + : _system(system), + _strategy(system), + _rho(_system, _strategy, -infinity()) { + _strategy.setRho(_rho); + } + + Domain solve(Variable& var) { + MaxExpression& rhs = *_system[var]; + + // _rho automatically keeps up to date with changes made to the + // strategy, so you don't need to stabilise it + + _strategy.get(rhs); + + + /* + do { + _strategy.hasChanged(false); + + solver_log::debug << "Stabilise assignment (toplevel)" << std::endl; + _rho.stabilise(); + + solver_log::debug << "Improve strategy (toplevel)" << std::endl; + // improve strategy + _strategy.get(rhs); + solver_log::debug << (_strategy.hasChanged() ? "Strategy has changed - loop again" : "Strategy has not changed - terminate") << std::endl; + } while (_strategy.hasChanged()); + */ + + return _rho[var]; + } private: const EquationSystem& _system; - mutable DynamicVariableAssignment* _rho; - mutable IdMap,unsigned int> _values; - mutable IdSet > _stable; - mutable IdMap,IdSet > > _influence; - mutable IdMap,IdSet > > _var_influence; + DynamicMaxStrategy _strategy; + DynamicVariableAssignment _rho; }; + /*template std::ostream& operator<<(std::ostream& cout, const MaxStrategy& strat) { strat.print(cout); diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp index 08c66ff..64ef096 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp @@ -1,6 +1,7 @@ #ifndef OPERATOR_HPP #define OPERATOR_HPP +#include #include template @@ -28,11 +29,6 @@ struct Maximum : public Operator { } }; - -template -T minimum(const T& l, const T& r) { - return (l < r ? l : r); -} template struct Minimum : public Operator { virtual Domain eval(const std::vector& arguments) const { @@ -40,7 +36,7 @@ struct Minimum : public Operator { for (typename std::vector::const_iterator it = arguments.begin(); it != arguments.end(); ++it) { - result = minimum(*it, result); //*it < result ? *it : result); + result = (*it < result ? *it : result); } return result; } @@ -52,8 +48,7 @@ struct Minimum : public Operator { template struct Negation : public Operator { virtual Domain eval(const std::vector& arguments) const { - if (arguments.size() > 1) - throw "Too many arguments to a negation."; + assert(arguments.size() == 1); return -arguments[0]; } void print(std::ostream& cout) const { diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp index ba5f650..746e5ef 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp @@ -7,7 +7,7 @@ template struct VariableAssignment { virtual ~VariableAssignment() { } - virtual const Domain& operator[](const Variable&) const = 0; + virtual const Domain operator[](const Variable& x) = 0; }; #include "EquationSystem.hpp" @@ -19,54 +19,73 @@ 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()), - _stable(system.variableCount()), + _values(system.variableCount(), value), + _unstable(system.variableCount()), _influence(system.variableCount(), IdSet >(system.variableCount())) { } - const Domain& operator[](const Variable& var) const { + const Domain operator[](const Variable& var) { solve(var); return _values[var]; } - void invalidate(const Variable& x) const { - solver_log::fixpoint << indent() << "Invalidating " << x << std::endl; - if (_stable.contains(x)) { - _stable.remove(x); + /*void stabilise() { + if (!_unstable.empty()) { + Variable& var = _system.variable(*_unstable.begin()); + solve(var); + } + }*/ + + void invalidate(const Variable& x) { + if (!_unstable.contains(x)) { + solver_log::fixpoint << indent() << "Invalidating " << x << std::endl; + + _unstable.insert(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 { - if (!_stable.contains(x)) { - _stable.insert(x); + void solve(const Variable& x) { + if (_unstable.contains(x)) { + _unstable.remove(x); solver_log::fixpoint << indent() << "Stabilise " << x << std::endl; stack_depth++; - if (!_system[x]) - return; - Domain val = _system[x]->evalWithStrat(DependencyAssignment(*this, x), - _strategy); + // we don't want the assignment to affect the strategy, so we're + // going to use a const reference here + const DynamicMaxStrategy& const_strat = _strategy; + DependencyAssignment assignment(*this, x); + Domain val = _system[x]->eval(assignment, const_strat); stack_depth--; if (val != _values[x]) { solver_log::fixpoint << x << " = " << val << std::endl; + + _strategy.invalidate(x); IdSet > oldInfluence = _influence[x]; _influence[x].clear(); _values[x] = val; - _strategy.invalidate(x); - - _stable.filter(oldInfluence); + _unstable.absorb(oldInfluence); for (typename IdSet >::iterator it = oldInfluence.begin(); it != oldInfluence.end(); @@ -74,31 +93,33 @@ private: solve(_system.variable(*it)); } } else { - solver_log::fixpoint << indent() << x << " did not change" << std::endl; + solver_log::fixpoint << indent() << x << " did not change: " + << x << " = " << val << std::endl; } } else { - solver_log::fixpoint << indent() << x << " is stable" << std::endl; + solver_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]; + const Domain operator[](const Variable& x) { + const Domain result = _assignment[x]; _assignment._influence[x].insert(_var); 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 > _unstable; + IdMap,IdSet > > _influence; }; #endif diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp index ac96107..3a82344 100644 --- a/clang/lib/Analysis/Interval.cpp +++ b/clang/lib/Analysis/Interval.cpp @@ -221,11 +221,6 @@ M merge_maps_with(const F& f, const M& left, const M& right) { return result; } -template<> -Vector minimum(const Vector& l, const Vector& r) { - return (l < r ? l : r); - return merge_maps_with(minimum, l, r); -} template T max(const T& l, const T& r) { return (l < r ? l : r); @@ -702,39 +697,15 @@ 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); + + Solver solver(system); 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"; + llvm::errs() << toString(var.name()) << " = " << toString(solver.solve(var)) << "\n"; } } diff --git a/impl/Expression.hpp b/impl/Expression.hpp index dcf7201..619bc7e 100644 --- a/impl/Expression.hpp +++ b/impl/Expression.hpp @@ -197,8 +197,7 @@ struct MaxExpression : public OperatorExpression { return this->_arguments[strat.get(*this)]->eval(rho, strat); } - unsigned int bestStrategy(VariableAssignment& rho, MaxStrategy& strat) const { - unsigned int bestIndex = const_cast&>(strat).get(*this); + unsigned int bestStrategy(VariableAssignment& rho, MaxStrategy& strat, unsigned int bestIndex) const { Domain bestValue = this->_arguments[bestIndex]->eval(rho, strat); for (unsigned int i = 0, length = this->_arguments.size(); diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp index 71ea4f4..6fee921 100644 --- a/impl/MaxStrategy.hpp +++ b/impl/MaxStrategy.hpp @@ -20,7 +20,7 @@ unsigned int stack_depth = 1; std::string indent() { std::string result = ""; for (unsigned int i = 0; i < stack_depth; ++i) { - result += '\t'; + result += ' '; } return result; } @@ -39,22 +39,13 @@ struct DynamicMaxStrategy : public MaxStrategy { _values(system.maxExpressionCount(), 0), _stable(system.maxExpressionCount()), _influence(system.maxExpressionCount(), - IdSet >(system.maxExpressionCount())), - _changed(false) + IdSet >(system.maxExpressionCount())) {} void setRho(DynamicVariableAssignment& rho) { _rho = ρ } - void hasChanged(bool c) { - _changed = c; - } - - bool hasChanged() const { - return _changed; - } - unsigned int get(const MaxExpression& e) const { log::strategy << indent() << "Look up " << e << std::endl; return _values[e]; @@ -99,32 +90,32 @@ struct DynamicMaxStrategy : public MaxStrategy { private: void solve(const MaxExpression& x) { if (!_stable.contains(x)) { + std::cerr << indent() << x.id() << std::endl; _stable.insert(x); log::strategy << indent() << "Stabilise " << x << std::endl; stack_depth++; DependencyAssignment assignment(*this, *_rho, x); DependencyStrategy depStrat(*this, x); - unsigned int val = x.bestStrategy(assignment, depStrat); + unsigned int val = x.bestStrategy(assignment, depStrat, _values[x]); stack_depth--; if (val != _values[x]) { + std::cerr << indent() << "-" << std::endl; log::strategy << x << " => " << *x.arguments()[val] << std::endl; - IdSet > oldInfluence = _influence[x]; - //_influence[x].clear(); _values[x] = val; - _changed = true; _rho->invalidate(*_system.varFromExpr(x)); //_rho->stabilise(); - _stable.filter(oldInfluence); - + IdSet > infl = _influence[x]; + _stable.filter(infl); + for (typename IdSet >::iterator - it = oldInfluence.begin(), - end = oldInfluence.end(); + it = infl.begin(), + end = infl.end(); it != end; ++it) { solve(_system.maxExpression(*it)); @@ -150,6 +141,7 @@ private: } const Domain operator[](const Variable& var) { // solve the strategy for this variable, too + // recursive magic! _strat.solve(*_strat._system[var]); _strat._influence[*_strat._system[var]].insert(_expr); return _rho[var]; @@ -186,7 +178,6 @@ private: IdMap,unsigned int> _values; IdSet > _stable; IdMap,IdSet > > _influence; - bool _changed; }; @@ -200,28 +191,12 @@ struct Solver { } Domain solve(Variable& var) { - MaxExpression& rhs = *_system[var]; - - // _rho automatically keeps up to date with changes made to the - // strategy, so you don't need to stabilise it - + MaxExpression& rhs = *_system[var]; + // this will automatically work sufficiently to get the final + // strategy for this variable's RHS _strategy.get(rhs); - - /* - do { - _strategy.hasChanged(false); - - log::debug << "Stabilise assignment (toplevel)" << std::endl; - _rho.stabilise(); - - log::debug << "Improve strategy (toplevel)" << std::endl; - // improve strategy - _strategy.get(rhs); - log::debug << (_strategy.hasChanged() ? "Strategy has changed - loop again" : "Strategy has not changed - terminate") << std::endl; - } while (_strategy.hasChanged()); - */ - + // this will automatically solve for the value of the RHS, if required return _rho[var]; } private: diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp index 2e081e6..e575d60 100644 --- a/impl/VariableAssignment.hpp +++ b/impl/VariableAssignment.hpp @@ -34,13 +34,6 @@ struct DynamicVariableAssignment : public VariableAssignment { return _values[var]; } - /*void stabilise() { - if (!_unstable.empty()) { - Variable& var = _system.variable(*_unstable.begin()); - solve(var); - } - }*/ - void invalidate(const Variable& x) { if (!_unstable.contains(x)) { log::fixpoint << indent() << "Invalidating " << x << std::endl; diff --git a/impl/main.cpp b/impl/main.cpp index 1fed389..be9cc82 100644 --- a/impl/main.cpp +++ b/impl/main.cpp @@ -159,8 +159,7 @@ int main (int argc, char* argv[]) { } } else { for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { - Variable& var = system.variable(i); - solver.solve(var); + solver.solve(system.variable(i)); } } clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &finish); diff --git a/impl/systems/test.eqns b/impl/systems/test.eqns index a3b521d..a320049 100644 --- a/impl/systems/test.eqns +++ b/impl/systems/test.eqns @@ -1,19 +1,19 @@ 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)) +neg-i-1-pre = max(-inf, neg-i-6[0], neg-i-2[0]) +i-1-pre = max(-inf, i-6[0], i-2[0]) +neg-i-5-pre = max(-inf, neg-i-1-pre) +i-5-pre = max(-inf, min(2, i-1-pre)) +neg-i-0-pre = max(-inf, min(-3, neg-i-1-pre)) +i-0-pre = max(-inf, i-1-pre) +neg-i-4-pre = max(-inf, neg-i-5-pre) +i-4-pre = max(-inf, min(1, i-5-pre)) +neg-i-3-pre = max(-inf, min(-2, neg-i-5-pre)) +i-3-pre = max(-inf, 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])) +neg-i-2-pre = max(-inf, neg-i-4[0], neg-i-3[0]) +i-2-pre = max(-inf, i-4[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)) diff --git a/impl/test/1.eqns b/impl/test/1.eqns index 0cdfd24..34c51de 100644 --- a/impl/test/1.eqns +++ b/impl/test/1.eqns @@ -1,3 +1,3 @@ -x = max(0, min(-1 + x, y)) y = max(0, 5 + x, x) z = max(0, 1 + z, 0 + x) +x = max(0, min(-1 + x, y)) diff --git a/impl/test/10.soln b/impl/test/10.soln index 20a47ca..238b7d5 100644 --- a/impl/test/10.soln +++ b/impl/test/10.soln @@ -1,9 +1,9 @@ -x = 0 -w = 0 -y = 0 -z = 0 -u = 0 a = 0 b = 0 c = 0 d = 0 +u = 0 +w = 0 +x = 0 +y = 0 +z = 0 diff --git a/impl/test/7.soln b/impl/test/7.soln index 0d85468..2c9b183 100644 --- a/impl/test/7.soln +++ b/impl/test/7.soln @@ -1,8 +1,8 @@ -x = 0 -y = 0 a = 0 b = 0 c = 0 d = 0 e = 0 f = 0 +x = 0 +y = 0 diff --git a/impl/test/8.soln b/impl/test/8.soln index 1945057..73d26df 100644 --- a/impl/test/8.soln +++ b/impl/test/8.soln @@ -1,4 +1,4 @@ -x = 0 w = 0 +x = 0 y = 0 z = 0 diff --git a/impl/test/9.soln b/impl/test/9.soln index 616c5e5..7116cf4 100644 --- a/impl/test/9.soln +++ b/impl/test/9.soln @@ -1,5 +1,5 @@ -x = 0 +u = 0 w = 0 +x = 0 y = 0 z = 0 -u = 0 diff --git a/impl/test/run b/impl/test/run index 169edda..d15fb68 100644 --- a/impl/test/run +++ b/impl/test/run @@ -7,15 +7,17 @@ FAILED=0 echo "Testing binary: $1 in directory $DIR" while [ -f "$DIR/$NUM.eqns" ] do + cat "$DIR/$NUM.soln" | sort > "/tmp/$NUM.soln.tmp" + mv "/tmp/$NUM.soln.tmp" "$DIR/$NUM.soln" 2> /dev/null OUTPUT=$(timeout 5s $1 "$DIR/$NUM.eqns" 2> /dev/null) if [ $? -eq 124 ]; then OUTPUT="did not terminate" fi - DIFF=$(echo "$OUTPUT" | diff - "$DIR/$NUM.soln") + DIFF=$(echo "$OUTPUT" | sort | diff - "$DIR/$NUM.soln") if [ ! -z "$DIFF" ]; then echo "==================" echo "Test #$NUM failed:" - echo "$OUTPUT" | sdiff - "$DIR/$NUM.soln" + echo "$OUTPUT" | sort | sdiff - "$DIR/$NUM.soln" echo FAILED=$(($FAILED + 1)) fi diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex index 66d5b4a..3d00b86 100644 --- a/tex/thesis/contribution/contribution.tex +++ b/tex/thesis/contribution/contribution.tex @@ -130,11 +130,31 @@ algorithm is presented in Listing \ref{algo:kleene}. 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, requiring the evaluation of -$O(n^3)$ right-hand-sides, and thus an approach which can evaluate -smaller portions of the system in each iteration would be a -significant improvement. +many right-hand-sides repeatedly for the same value. Thus an +approach which can evaluate smaller portions of the system in each +iteration would be a significant improvement. + +An additional deficiency of Kleene iteration is that it is not +guaranteed to terminate. In some cases Kleene iteration must iterate +an infinite number of times in order to reach a fixpoint. An example +system is presented as Figure \ref{fig:kleene-infinite}. In this case +$x$ will take the value of $0$ in the first iteration, then $y$ will +evaluate to $-1$. In the next iteration $x$ will also take the value +$-1$, thereby requiring $y$ to take the value $-2$. This will continue +without bound, resulting in the Kleene iteration never reaching the +greatest fixpoint of $\{ x \mapsto -\infty, y \mapsto -\infty \}$. + +\begin{figure}[H] + \begin{align*} + x &= \min(0, x) \\ + y &= x - 1 + \end{align*} + \caption{An example equation system for which Kleene iteration will + not terminate} + \label{fig:kleene-infinite} +\end{figure} -\subsection{W-DFS algorithm} \ref{sec:wdfs} +\subsection{W-DFS algorithm} \label{sec:wdfs} 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 @@ -255,7 +275,7 @@ problem it is possible \end{algorithm} -\subsection{Adapted W-DFS algorithm} \ref{sec:adapted-wdfs} +\subsection{Adapted W-DFS algorithm} \label{sec:adapted-wdfs} This, then, allows us to use the W-DFS algorithm to re-evaluate only those parts of the strategy which have changed. Listing -- cgit v1.2.3