diff options
Diffstat (limited to 'tex/thesis/contribution')
| -rw-r--r-- | tex/thesis/contribution/contribution.tex | 255 |
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} |