summaryrefslogtreecommitdiff
path: root/tex/thesis/contribution/contribution.tex
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis/contribution/contribution.tex')
-rw-r--r--tex/thesis/contribution/contribution.tex255
1 files changed, 120 insertions, 135 deletions
diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index fac83c9..9e90749 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -57,8 +57,8 @@ 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 discuss a modification
of the algorithm to allow it to perform $\max$-strategy iteration. The
-chapter will conclude with our Local Demand-driven Strategy
-Improvement (LDSI) algorithm to perform efficient strategy iteration
+chapter will conclude with our Demand-driven Strategy
+Improvement (DSI) algorithm to perform efficient strategy iteration
and fixpoint iteration. % TODO: fix me, or something
The existing algorithm as presented in Section
@@ -355,10 +355,6 @@ values, as they may change their value if re-evaluated (and hence are
not certainly stable). If these values change then they, too, will
destabilise their dependent variables, and so on.
-The W-DFS algorithm provides us with a \emph{local},
-\emph{demand-driven} solver for greatest fixpoints of monotonic
-fixpoint problems.
-
\begin{figure}[tbphH]
\begin{tikzpicture}
\node[draw] (full) at (0,-2) {
@@ -415,9 +411,7 @@ 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 subsystem unevaluated. We call this algorithm \emph{local},
-because it considers only as many variables as are necessary to
-compute the requested values.
+other subsystem unevaluated.
@@ -647,7 +641,7 @@ particular $\improve$ that we are using (see Listing \ref{algo:pmax})
satisfies this property using an anonymous function to delay the
computation.
-\section{Local Demand-driven Strategy Improvement (LDSI)}
+\section{Demand-driven Strategy Improvement (DSI)}
W-DFS speeds up both the $\max$-strategy iteration and the fixpoint
iteration as two independent processes, but each time we improve our
@@ -659,8 +653,8 @@ parts of the system have changed we can jump in partway through the
process of finding a fixpoint, thereby avoiding repeating
calculations.
-The new \emph{Local Demand-driven Strategy Improvement} algorithm,
-\emph{LDSI}, seeks to do this. By adding an ``invalidate'' procedure
+The new \emph{Demand-driven Strategy Improvement} algorithm,
+\emph{DSI}, seeks to do this. By adding an ``invalidate'' procedure
to the fixpoint iteration we provide a method for the $\max$-strategy
to invalidate fixpoint variables, and we modify the fixpoint iteration
algorithm to report which variables it has modified with each fixpoint
@@ -674,12 +668,6 @@ changed variables to determine which portions of the current strategy
are now unstable. This process continues until the $\max$-strategy
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}, considering only the subset of variables necessary to
-calculate the values we are interested in..
-
@@ -753,7 +741,7 @@ This algorithm is presented in three parts.
\end{tabularx}
\EndGlobals
\end{algorithmic}
- \caption{Global variables used by the LDSI algorithm}
+ \caption{Global variables used by the DSI algorithm}
\label{algo:ldsi:globals}
\end{algorithm}
@@ -918,6 +906,114 @@ being stabilised.
+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) = \{
+\rho \mid \rho = s(\rho) \}$, then we find that $\solnFP(s) \in \fix(s)$
+and $\solnFP(s) \ge \rho ~ \forall \rho \in \fix(s)$. Our general
+approach will be to consider our variable assignment $D \ge \solnFP(s)$
+and show that it decreases until $D \in \fix(s)$ and thus $D =
+\solnFP(s)$.
+
+We have three invariants for the fixpoint portion of the DSI
+algorithm. We use $\depFP^{+}(x)$ to be the set of all variables which
+$x$ may depend on. $\depFP^{+}$ is defined as the transitive closure
+of $\depFP$, $\depFP[x] = \{ y \in X \mid
+x \in \inflFP[y] \}$. $\RFP \subseteq X$ is defined as the variables
+currently on our recursion stack.
+\begin{align}
+ D &\ge \solnFP(s) \label{eqn:fp-inv1} \\
+%
+ x &\in \inflFP[y] & \forall x \in \stableFP, y \in \depFP[x]
+ \label{eqn:fp-inv3} \\
+%
+ D &= \solnFP(s)[x] & \mbox{if }
+ x \not \in \RFP,
+ \depFP^{+}[x] \cap \RFP = \emptyset,
+ x \in \stableFP
+ \label{eqn:fp-inv2}
+\end{align}
+
+(\ref{eqn:fp-inv1}) follows from monotonicity. We begin our iteration
+at some variable assignment $D \ge \solnFP(s)$ and monotonically descend
+from there. We know that $s(D)[x] \ge soln(s)[x] ~\forall D \ge
+\solnFP(s), x \in X$, thus each evaluation of $s[x]$ in the context of
+$D$ will result in a new value for $D[x]$ which is either closer to or
+equal to $\solnFP(s)[x]$. As we only ever evaluate in the context of
+variables taken from $D$, and $D[x]$ is set to $\infty$ when $x$ is
+invalidated, we know that $D \ge \solnFP(s)$ holds.
+
+(\ref{eqn:fp-inv3}) follows from the use of the $\eval \fixpoint$
+function. Each variable lookup results in a direct insertion into
+$\inflFP$, so during the evaluation of $x$ all relevant $\inflFP$ sets
+are updated to reflect the current dependencies.
+
+For (\ref{eqn:fp-inv2}) we will examine what has happened when each of
+the conditions is false:
+\begin{itemize}
+\item
+ If $x \in \RFP$ then we are currently in the context of an earlier
+ evaluation of $x$, so the value of $D[x]$ will be changed again by
+ that earlier call. In addition, we conclude that $x \in
+ \depFP^{+}[x]$ and thus, from the following condition, that $x$ will
+ be re-evaluated at some point after this one.
+
+\item
+ If $\depFP^{+}[x] \cap \RFP \ne \emptyset$ then a variable which $x$
+ depends on is in $\RFP$ at the moment. This will result in the
+ re-evaluation of $x$ if the value of any of the variables in
+ $\depFP^{+}[x] \cap \RFP$ have changed.
+
+\item
+ If $x \not \in \stableFP$ then a re-evaluation of $x$ will occur
+ with the next call to $\solve \fixpoint(x)$. This may result in a
+ change to the value of $D[x]$, or it may leave $D[x]$ stable for the
+ moment. If we denote the variable assignment before the evaluation
+ of $x$ by $D_{\pre}$, and the variable assignment after the
+ evaluation of $x$ by $D_{\post}$ then we find that $D_{\post} \le
+ D_{\pre}$, due to the monotonicity of $s$. After each change of
+ $D[x]$, everything which \emph{may} have depended on $D[x]$ is
+ re-evaluated (see the previous two items), leading to a final point
+ of stability when $D[x] = \solnFP(s)[x]$, by the definition of
+ $\solnFP(s)[x]$ and (\ref{eqn:fp-inv1}).
+\end{itemize}
+
+After an evaluation of $\solve \fixpoint(x)$ we know that $x \in
+\stableFP$. If it is also the case that $\RFP = \emptyset$, as is the
+case for top-level calls to $\solve \fixpoint$, then we know that
+$D[x] = \solnFP(s)[x]$. This means that the function $\lambda x
+. (\solve \fixpoint(x); D[x])$ will act as a variable assignment
+solving for the greatest fixpoint of $s = \sigma(\system)$, as is
+required by our $\max$-strategy iteration. As the $\max$-strategy
+iteration changes $\sigma$ it also induces a change in $s =
+\sigma(\system)$, so in order to maintain the correctness of this
+algorithm we must show that our above invariants are maintained by
+this process.
+
+When the $\max$-strategy iteration changes the current $\max$-strategy
+$\sigma$ at the variable $x$ it changes the equation system $s =
+\sigma(\system)$ that the fixpoint iteration uses. The $\max$-strategy
+iteration then invalidates the affected portion of the fixpoint
+iteration by doing two things: it removes the variable $x$ from the
+$\stableFP$ set, and it sets $D[x] = \infty$. The invalidation of
+variables is then propagated to each variable which transitively
+depends on $x$: $\{ y \in X \mid x \in \depFP^{+}[y] \} = \{ y \in X
+\mid y \in \inflFP^{+}[x] \}$, where $\inflFP^{+}$ is the transitive
+closure of $\inflFP$. We know from (\ref{eqn:fp-inv3}) that this
+transitive closure of $\inflFP$ will identify the entire subsystem
+which may depend on the value of $x$. The invalidation of transitive
+dependencies ensures that (\ref{eqn:fp-inv1}) holds for the changed
+subsystem, as $\infty \ge z ~ \forall z \in \CZ$. From
+(\ref{eqn:fp-inv1}) we can then conclude that (\ref{eqn:fp-inv2})
+holds as well, as the removal of $x$ from $\stableFP$ combined with
+(\ref{eqn:fp-inv1}) leads to (\ref{eqn:fp-inv2}). These invariants now
+hold for the affected sub-system and are still true for the unaffected
+sub-system. Thus our invariants hold for our entire system and our
+fixpoint iteration will continue to be correct in the presence of
+invalidation by the $\max$-strategy iteration.
+
+
+
\subsection{$\max$-strategy iteration} \label{sec:ldsi:max-strategy}
@@ -1029,122 +1125,14 @@ Section \ref{sec:adapted-wdfs}.
-
-\subsection{Correctness} \label{sec:ldsi:correctness}
-
-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) = \{
-\rho \mid \rho = s(\rho) \}$, then we find that $\solnFP(s) \in \fix(s)$
-and $\solnFP(s) \ge \rho ~ \forall \rho \in \fix(s)$. Our general
-approach will be to consider our variable assignment $D \ge \solnFP(s)$
-and show that it decreases until $D \in \fix(s)$ and thus $D =
-\solnFP(s)$.
-
-We begin by stating three invariants of the LDSI algorithm. We use
-$\depFP^{+}(x)$ to be the set of all variables which $x$ may depend
-on. $\depFP^{+}$ is defined as the transitive closure of $\depFP$,
-$\depFP[x] = \{ y \in X \mid x \in \inflFP[y] \}$. $\RFP \subseteq X$
-is defined as the variables currently on our recursion stack.
-\begin{align}
- D &\ge \solnFP(s) \label{eqn:fp-inv1} \\
-%
- x &\in \inflFP[y] & \forall x \in \stableFP, y \in \depFP[x]
- \label{eqn:fp-inv3} \\
-%
- D &= \solnFP(s)[x] & \mbox{if }
- x \not \in \RFP,
- \depFP^{+}[x] \cap \RFP = \emptyset,
- x \in \stableFP
- \label{eqn:fp-inv2}
-\end{align}
-
-(\ref{eqn:fp-inv1}) follows from monotonicity. We begin our iteration
-at some variable assignment $D \ge \solnFP(s)$ and monotonically descend
-from there. We know that $s(D)[x] \ge soln(s)[x] ~\forall D \ge
-\solnFP(s), x \in X$, thus each evaluation of $s[x]$ in the context of
-$D$ will result in a new value for $D[x]$ which is either closer to or
-equal to $\solnFP(s)[x]$. As we only ever evaluate in the context of
-variables taken from $D$, and $D[x]$ is set to $\infty$ when $x$ is
-invalidated, we know that $D \ge \solnFP(s)$ holds.
-
-(\ref{eqn:fp-inv3}) follows from the use of the $\eval \fixpoint$
-function. Each variable lookup results in a direct insertion into
-$\inflFP$, so during the evaluation of $x$ all relevant $\inflFP$ sets
-are updated to reflect the current dependencies.
-
-For (\ref{eqn:fp-inv2}) we will examine what has happened when each of
-the conditions is false:
-\begin{itemize}
-\item
- If $x \in \RFP$ then we are currently in the context of an earlier
- evaluation of $x$, so the value of $D[x]$ will be changed again by
- that earlier call. In addition, we conclude that $x \in
- \depFP^{+}[x]$ and thus, from the following condition, that $x$ will
- be re-evaluated at some point after this one.
-
-\item
- If $\depFP^{+}[x] \cap \RFP \ne \emptyset$ then a variable which $x$
- depends on is in $\RFP$ at the moment. This will result in the
- re-evaluation of $x$ if the value of any of the variables in
- $\depFP^{+}[x] \cap \RFP$ have changed.
-
-\item
- If $x \not \in \stableFP$ then a re-evaluation of $x$ will occur
- with the next call to $\solve \fixpoint(x)$. This may result in a
- change to the value of $D[x]$, or it may leave $D[x]$ stable for the
- moment. If we denote the variable assignment before the evaluation
- of $x$ by $D_{\pre}$, and the variable assignment after the
- evaluation of $x$ by $D_{\post}$ then we find that $D_{\post} \le
- D_{\pre}$, due to the monotonicity of $s$. After each change of
- $D[x]$, everything which \emph{may} have depended on $D[x]$ is
- re-evaluated (see the previous two items), leading to a final point
- of stability when $D[x] = \solnFP(s)[x]$, by the definition of
- $\solnFP(s)[x]$ and (\ref{eqn:fp-inv1}).
-\end{itemize}
-
-After an evaluation of $\solve \fixpoint(x)$ we know that $x \in
-\stableFP$. If it is also the case that $\RFP = \emptyset$, as is the
-case for top-level calls to $\solve \fixpoint$, then we know that
-$D[x] = \solnFP(s)[x]$. This means that the function $\lambda x
-. (\solve \fixpoint(x); D[x])$ will act as a variable assignment
-solving for the greatest fixpoint of $s = \sigma(\system)$, as is
-required by our $\max$-strategy iteration. As the $\max$-strategy
-iteration changes $\sigma$ it also induces a change in $s =
-\sigma(\system)$, so in order to maintain the correctness of this
-algorithm we must show that our above invariants are maintained by
-this process.
-
-When the $\max$-strategy iteration changes the current $\max$-strategy
-$\sigma$ at the variable $x$ it changes the equation system $s =
-\sigma(\system)$ that the fixpoint iteration uses. The $\max$-strategy
-iteration then invalidates the affected portion of the fixpoint
-iteration by doing two things: it removes the variable $x$ from the
-$\stableFP$ set, and it sets $D[x] = \infty$. The invalidation of
-variables is then propagated to each variable which transitively
-depends on $x$: $\{ y \in X \mid x \in \depFP^{+}[y] \} = \{ y \in X
-\mid y \in \inflFP^{+}[x] \}$, where $\inflFP^{+}$ is the transitive
-closure of $\inflFP$. We know from (\ref{eqn:fp-inv3}) that this
-transitive closure of $\inflFP$ will identify the entire subsystem
-which may depend on the value of $x$. The invalidation of transitive
-dependencies ensures that (\ref{eqn:fp-inv1}) holds for the changed
-subsystem, as $\infty \ge z ~ \forall z \in \CZ$. From
-(\ref{eqn:fp-inv1}) we can then conclude that (\ref{eqn:fp-inv2})
-holds as well, as the removal of $x$ from $\stableFP$ combined with
-(\ref{eqn:fp-inv1}) leads to (\ref{eqn:fp-inv2}). These invariants now
-hold for the affected sub-system and are still true for the unaffected
-sub-system. Thus our invariants hold for our entire system and our
-fixpoint iteration will continue to be correct in the presence of
-invalidation by the $\max$-strategy iteration.
-
-
-We move now to the $\max$-strategy iteration. We will use $\rho: X \to
-\CZ$ as $\rho = \lambda x . (\solve \fixpoint(x); D[x])$, a variable
+In the following brief analysis we use $\rho: X \to \CZ$ as $\rho
+= \lambda x . (\solve \fixpoint(x); D[x])$ to denote a variable
assignment which will always calculate the greatest fixpoint of
$\sigma(\system)$ for the current strategy $\sigma$. Each time $\rho$
is queried for a variable's value it will also record which variables
have had their values changed, whether or not those changed values are
-final, in the set $\touchedFP$.
+final, in the set $\touchedFP$. This represents the effect of the
+fixpoint iteration portion of the DSI algorithm.
We can establish similar invariants for the $\max$-strategy iteration
as we had for the fixpoint iteration. We denote the optimal strategy
@@ -1188,9 +1176,6 @@ the $\max$-strategy. If the variable has stabilised to the same value
as it had previously then it has not changed and thus has no effect on
the $\max$-strategy.
-If both the $\max$-strategy iteration and the fixpoint iteration
-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}