summaryrefslogtreecommitdiff
path: root/tex/thesis
diff options
context:
space:
mode:
authorZancanaro; Carlo <czan8762@plang3.cs.usyd.edu.au>2012-11-01 18:06:13 +1100
committerZancanaro; Carlo <czan8762@plang3.cs.usyd.edu.au>2012-11-01 18:06:13 +1100
commitb7eaa99578037789a337c5061c0ea8ee3150b63c (patch)
treee63a023a85ef167760f55229c1d96fbcaaa1c64e /tex/thesis
parente207a8fec1bae01068bdb3a27a2090a4af5f8cb2 (diff)
A bunch of fixes to the solver, and moving it in to clang.
Also some contribution writing stuff. Basically: lots of work.
Diffstat (limited to 'tex/thesis')
-rw-r--r--tex/thesis/contribution/contribution.tex30
1 files changed, 25 insertions, 5 deletions
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