summaryrefslogtreecommitdiff
path: root/tex/thesis/contribution
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis/contribution')
-rw-r--r--tex/thesis/contribution/contribution.tex102
1 files changed, 53 insertions, 49 deletions
diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index 48a5e73..fac83c9 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -50,8 +50,8 @@ In this chapter the main theoretical contribution of this thesis is
presented: an extension on a $\max$-strategy iteration algorithm for
solving fixpoint equations over the integers with monotonic
operators\cite{Gawlitza:2007:PFC:1762174.1762203} (see Section
-\ref{sec:gawlitza-algorithm}). We devise an algorithm which runs in
-linear time in the best case.
+\ref{sec:gawlitza-algorithm}). We devise an algorithm which performs
+considerably better for practical equation systems.
In this chapter we will begin by presenting the Work-list Depth First
Search (W-DFS) fixpoint algorithm developed by Seidl et
@@ -135,7 +135,7 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$.
\begin{definition}
\textbf{Equation System:} An equation system is a mapping from
variables to expressions. $\system : X \to E$. We define
- $E_\system \subset E$ to be the preimage of system, that is
+ $E_\system \subset E$ to be the preimage of $\system$, that is
$E_\system = \{ e \in E \mid system(x) = e, \forall x \in X \}$. As
each element of $E$ is also a function $(X \to \CZ) \to \CZ$, so an
equation system is considered as a function $\system : X \to
@@ -170,16 +170,6 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$.
\end{align*}
\end{definition}
-\begin{definition}
- A variable or expression $x$ is said to \textbf{depend} on $y$ if
- $x(\rho) \ne x(\varrho)$ and
- \begin{align*}
- \rho(z) &= \varrho(z) & \forall z \in X \backslash \{y\} \\
- \rho(y) &\ne \varrho(y)
- \end{align*}
-
- If $x$ depends on $y$ then $y$ is said to \emph{influence} $x$.
-\end{definition}
\section{Fixpoint Iteration}
\subsection{Kleene Iteration}
@@ -191,7 +181,7 @@ 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}.
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
\begin{algorithmic}
\Function {solvefixpoint} {$\system \in \Systems$}
\State $k = 0$
@@ -223,7 +213,7 @@ iteration will continue without bound, tending towards $\{ x \mapsto
-\infty, y \mapsto 0 \}$ rather than the greatest fixpoint of $\{
x \mapsto -\infty, y \mapsto -\infty \}$.
-\begin{figure}[H]
+\begin{figure}[tbphH]
\begin{align*}
x &= \min(0, x - 1) \\
y &= \min(0, \infty \oplus x) &
@@ -240,15 +230,41 @@ at most restricted to $|X|$ iterations in the particular case of the
$\max$-strategy iteration algorithm considered in this thesis. Kleene
iteration is therefore restricted to $\Theta(|X|^3)$ right hand side
evaluations at most in our application. We seek to improve on this
-performance in the next section.
+performance in the next section by taking into account dependencies
+between expressions.
+
+\begin{definition}
+ An expression $x$ is said to \textbf{depend} on $y$ if and only if
+ $x(\rho) \ne x(\varrho)$ and
+ \begin{align*}
+ \rho(z) &= \varrho(z) & \forall z \in X \backslash \{y\} \\
+ \rho(y) &\ne \varrho(y)
+ \end{align*}
+
+ Intuitively, $x$ depends on $y$ if and only if a change in the value
+ of $y$ induces a change in the value of $x$.
+
+ If $x$ depends on $y$ then $y$ is said to \emph{influence} $x$.
+\end{definition}
+
\subsection{W-DFS algorithm} \label{sec:wdfs}
-The W-DFS algorithm of Seidl et al.~takes into account dependencies
-between variables as it solves the system. By taking into account
-dependencies we can leave portions of the system unevaluated when we
-are certain that those values have not changed. The algorithm is
-presented in Listing \ref{algo:wdfs}.
+Several algorithms have been presented in literature for finding
+solutions to general fixpoint equation systems. In particular has been
+the \emph{topdown solver} of Charlier and Van
+Hentenryck\cite{TD-fixpoint} and the \emph{worklist} solver of
+Kildall\cite{Kildall:1973:UAG:512927.512945} which has been further
+extended by others\cite{Jorgensen94findingfixpoints,FP-efficient}. The
+W-DFS algorithm of Seidl et al.\cite{DBLP:tr/trier/MI96-11} is an
+attempt to combine the best aspects of these general fixpoint
+algorithms.
+
+The W-DFS algorithm takes into account dependencies between variables
+as it solves the system. By taking into account dependencies we can
+leave portions of the system unevaluated when we are certain that
+those values have not changed. The algorithm is presented in Listing
+\ref{algo:wdfs}.
\begin{algorithm}
\begin{algorithmic}
@@ -343,7 +359,7 @@ The W-DFS algorithm provides us with a \emph{local},
\emph{demand-driven} solver for greatest fixpoints of monotonic
fixpoint problems.
-\begin{figure}[H]
+\begin{figure}[tbphH]
\begin{tikzpicture}
\node[draw] (full) at (0,-2) {
\begin{minipage}{0.3\textwidth}
@@ -399,14 +415,10 @@ other subsystem. To compute the value of $x$ in the greatest fixpoint
it is unnecessary to compute the value of the variable $d$, but it is
necessary to compute the value of $y$. The W-DFS algorithm, will only
evaluate the necessary subsystem for a requested variable, leaving the
-other system unevaluated. In order to capture this property we will
-define the notion of a \emph{local} solver.
+other subsystem unevaluated. We call this algorithm \emph{local},
+because it considers only as many variables as are necessary to
+compute the requested values.
-\begin{definition}
- \textbf{Local:} A solver is said be \emph{local} if, for some
- equation system, $\system$, and some $e \in E_\system$, it will
- solve for $e_x$ without evaluating every element of $E_\system$.
-\end{definition}
\section{$\max$-strategy Iteration}
@@ -475,7 +487,7 @@ approach is to perform a loop, improving the strategy at each step,
until an equilibrium point is reached. The approach is presented in
Listing \ref{algo:naive-strategy}.
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
\begin{algorithmic}
\Assumptions
\begin{tabularx}{0.9\textwidth}{rX}
@@ -526,7 +538,7 @@ the W-DFS algorithm presented above in Section \ref{sec:wdfs}. Listing
\ref{algo:adapted-wdfs} presents one variation on W-DFS to solve
$\max$-strategy iteration problems.
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
\begin{algorithmic}
\Globals
\begin{tabularx}{0.9\textwidth}{rX}
@@ -665,7 +677,8 @@ stabilises (at which point the fixpoint will also stabilise).
Both portions of the LDSI algorithm are \emph{demand driven}, and so
any necessary evaluation of strategies or fixpoint values is delayed
until the point when it is required. This means that the solver will
-be \emph{local} (see Section \ref{sec:wdfs}).
+be \emph{local}, considering only the subset of variables necessary to
+calculate the values we are interested in..
@@ -701,7 +714,7 @@ This algorithm is presented in three parts.
\subsection{Top level} \label{sec:ldsi:top-level}
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
\begin{algorithmic}
\Globals
\begin{tabularx}{0.9\textwidth}{rX}
@@ -749,7 +762,7 @@ in Sections \ref{sec:wdfs} and \ref{sec:adapted-wdfs}. The only
exception is $\touchedFP$, which is a newly introduced variable to
track variables which are touched by the fixpoint iteration steps.
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
\begin{algorithmic}
\Function {init} {$s \in \Systems$}
\State $D = \underline{-\infty}$
@@ -803,7 +816,7 @@ have already been computed to avoid performing additional work. The
last stable value is stored in this procedure to identify
\emph{changed} values, rather than only \emph{unstable} ones.
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
\begin{algorithmic}
\Function {evalfixpoint} {$x \in X$, $y \in X$}
\State $\solve \fixpoint(y)$
@@ -822,7 +835,7 @@ algorithm, except for the fact that $\solve$ has been renamed to
$\solve \fixpoint$. $\eval \fixpoint$ performs the same function as
the $\eval$ function in Listing \ref{algo:wdfs}.
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
\begin{algorithmic}
\Procedure {invalidatefixpoint} {$x \in X$}
\Comment{Invalidate a fixpoint variable}
@@ -863,7 +876,7 @@ set of changed variables for the $\max$-strategy iteration phase.
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
\begin{algorithmic}
\Procedure {solvefixpoint} {$x \in X$}
\If {$x \not \in \stableFP$}
@@ -909,7 +922,7 @@ being stabilised.
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
\begin{algorithmic}
\Function {evalstrategy} {$x \in E_{\max}$, $y \in E_{\max}$}
\State $\solve \strategy(y)$
@@ -957,7 +970,7 @@ directly, but if it is dependent on its own value (as in $\{ x = x + 1
\}$, for example), then it will be destabilised by the transitivity of
$\invalidate \strategy$.
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
\begin{algorithmic}
\Procedure {invalidatestrategy} {$x \in E_{\max}$}
\If {$x \in \stableSI$}
@@ -982,7 +995,7 @@ by a $\solve \strategy$ call. All $\max$-expressions which
(transitively) depend on $x$ are destabilised recursively.
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
\begin{algorithmic}
\Procedure {solvestrategy} {$x \in E_{\max}$}
\If {$x \not \in \stableSI$}
@@ -1019,13 +1032,6 @@ Section \ref{sec:adapted-wdfs}.
\subsection{Correctness} \label{sec:ldsi:correctness}
-To argue the correctness of our LDSI algorithm we will first argue the
-correctness of the fixpoint iteration portion of the algorithm. We
-will then argue the correctness of the $\max$-strategy iteration
-portion, including the communication between the fixpoint iteration
-and $\max$-strategy iteration.
-
-
The fixpoint iteration portion of the algorithm is concerned with
finding the greatest fixpoint, $\solnFP(s) : X \to D$ for the system $s
= \sigma(\system)$. If we consider all valid fixpoints, $\fix(s) = \{
@@ -1187,6 +1193,4 @@ correctly solve their respective portions of the problem, and the
communication between them is correct, then we know that the overall
algorithm is correct.
-
\subsection{Implementation} \label{sec:ldsi:implementation}
-