Thesis thesis thesis.

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}