diff options
Diffstat (limited to 'tex/thesis/contribution')
| -rw-r--r-- | tex/thesis/contribution/contribution.tex | 314 |
1 files changed, 157 insertions, 157 deletions
diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex index ff75e9b..18d956f 100644 --- a/tex/thesis/contribution/contribution.tex +++ b/tex/thesis/contribution/contribution.tex @@ -145,7 +145,7 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$. \begin{definition} \textbf{Dependencies:} A variable or expression $x$ is said to - \emph{depend on} $y$ if $x(\rho) \ne x(\varrho)$, when + \emph{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) @@ -154,12 +154,6 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$. If $x$ depends on $y$ then $y$ is said to \emph{influence} $x$. \end{definition} -\begin{definition} - \textbf{Local:} A solver is said be 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{Fixpoint Iteration} \subsection{Kleene Iteration} @@ -187,28 +181,20 @@ algorithm is presented in Listing \ref{algo:kleene}. \label{algo:kleene} \end{algorithm} -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 -many right-hand-sides repeatedly for the same value. Thus an +For each iteration the entire system is evaluated, resulting in a +considerable inefficiency in practice, requiring the repeated +evaluation of many right-hand-sides 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 for all fixpoints. An example system is -presented in Figure \ref{fig:kleene-infinite}. In this case our first -iteration will give us $\{ x \mapsto 0, y \mapsto 0 \}$, leading to a -second iteration resulting in $\{ x \mapsto -1, y \mapsto 0\}$. This -will continue without bound resulting - -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 \}$. +presented in Figure \ref{fig:kleene-infinite}, where our first +iteration will give $\{ x \mapsto 0, y \mapsto 0 \}$, leading to a +second iteration resulting in $\{ x \mapsto -1, y \mapsto 0\}$. The +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{align*} @@ -226,25 +212,25 @@ significant problem in our application, however, as it has been shown in the work of Gawlitza et al.\cite{Gawlitza:2007:PFC:1762174.1762203}, that Kleene iteration in this specific case is restricted to at most $|X|$ iterations. It does, -however, require $\Theta(|X|)$ right hand side evaluations, which is +however, require $\Theta(|X|^3)$ right hand side evaluations, which is very inefficient. \subsection{W-DFS algorithm} \label{sec:wdfs} -The W-DFS algorithm of Seidl et al.~takes into account some form of -data-dependencies as it solves the system. This gives it the ability -to leave portions of the system unevaluated when it is certain that -those values have not changed. The algorithm is presented in Listing -\ref{algo: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 it can leave portions of the system unevaluated when it +is certain that those values have not changed. The algorithm is +presented in Listing \ref{algo:wdfs}. \begin{algorithm} \begin{algorithmic} \Globals \begin{tabularx}{0.9\textwidth}{rX} - $D$ & $\in X \to \CZ$, a mapping from variables to their current + $D$ & $: X \to \CZ$, a mapping from variables to their current values \\ - $\inflFP$ & $\in X \to 2^X$, a mapping from a variable to the + $\inflFP$ & $: X \to 2^X$, a mapping from a variable to the variables it \emph{may} influence \\ $\stableFP$ & $\subseteq X$, a set of ``stable'' variables \\ @@ -300,11 +286,12 @@ those values have not changed. The algorithm is presented in Listing \label{algo:wdfs} \end{algorithm} -The function $\init$ in Listing \ref{algo:wdfs:init} is of the type -$\Systems \to (X \to D)$. It takes an equation system and returns a -function to query the greatest fixpoint. Each fixpoint value is solved -on demand and will only evaluate the subset of the equation system -which is required to ensure the correct solution is found. +The function $\init: \Systems \to (X \to D)$ in +Listing \ref{algo:wdfs:init} takes an equation system as its argument +and returns a function to query the greatest fixpoint. Each fixpoint +value is solved on demand and will only evaluate the subset of the +equation system which is required to ensure the correct solution is +found. The algorithm performs no evaluation of any variables unless their value is requested (whether externally or internally). Once a value is @@ -312,10 +299,10 @@ requested the right-hand-side is evaluated, which may in turn request the values of other variables (through the $\eval$ function). In the case of mutually-recursive variables this would result in -infinite recursion, as each time the variable's value must be -calculated it must first calculate its own value. In order to prevent -this a $\stable$ set is maintained of variables whose values are -either currently being computed or whose values have already been +infinite recursion, as each time the variable's value is calculated we +must first calculate the variable's value. In order to prevent this a +$\stable$ set is maintained of variables whose values are either +currently being computed or whose values have already been computed. This set provides a ``base'' for the recursion to terminate, at which point the value is simply looked up in $D$. @@ -329,12 +316,7 @@ The W-DFS algorithm provides us with a \emph{local}, \emph{demand-driven} solver for greatest fixpoints of monotonic fixpoint problems. -Because each value is only computed when requested, the solver avoids -calculating results which are irrelevant to the final outcome. To -provide a more tangible example, consider the equation system -presented in Figure \ref{fig:wdfs-example}. - -\begin{figure} +\begin{figure}[H] \begin{align*} x &= \min(0, y) \\ y &= x \\ @@ -348,22 +330,29 @@ presented in Figure \ref{fig:wdfs-example}. \label{fig:wdfs-example} \end{figure} -It is clear by inspecting this system that it could be split into two -equation systems, one consisting of $\{x, y\}$ and the other of $\{a, -b, c, d, e\}$. In order to find the value of a variable in either of -these sub-systems it is necessary to evaluate the entire sub-system, -but it is not necessary to evaluate the other sub-system. So, for -example, to find the value of $x$ in the greatest fixpoint it is -unnecessary to find the value of the variable $d$. - -W-DFS, in this case, would only evaluate the sub-system containing the -requested variable and would leave the other sub-system entirely -unsolved until a variable within it has its value requested. - -This means that W-DFS can avoid evaluating a large portion of some -equation systems, thereby making it a \emph{local} solver. +Because each value is only computed when requested, the solver avoids +calculating results which are irrelevant to the final outcome. To +provide a more concrete example, consider the equation system +presented in Figure \ref{fig:wdfs-example}. This equation system can +be separated into two independent equation systems, one consisting of +$\{x, y\}$ and the other of $\{a, b, c, d, e\}$. In order to find the +value of a variable in either of these sub-systems it is necessary to +evaluate the entire sub-system, but it is not necessary to evaluate +the other sub-system. 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 untouched. In order to capture this property +we will define the notion of a \emph{local} solver. +\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} +W-DFS provides us with a \emph{local}, \emph{demand-driven} solver for +greatest-fixpoint problems. @@ -371,26 +360,25 @@ equation systems, thereby making it a \emph{local} solver. The problem of $\max$-strategy iteration is trying to find a mapping $\sigma: E_{\max} \to E$ from each $\max$-expression to its greatest -sub-expression. (We will also use $\sigma: \Systems \to \Systems$ as a +sub-expression. We will use $\sigma: \Systems \to \Systems$ as a shorthand to denote the system obtained by replacing each -$\max$-expression, $x$, in $\system$ with $\sigma(x)$.) +$\max$-expression, $x$, in $\system$ with $\sigma(x)$. In the particular case of \emph{monotonic}, \emph{expansive} operators it has been shown\cite{Gawlitza:2007:PFC:1762174.1762203} that this process will take a finite number of iterations if we ensure at each iteration that we make a \emph{strict} improvement on our strategy. This means that each time we improve our strategy we must -make it \emph{better} in at least one $\max$-expression, and no worse -in the others. +make it greater in at least one $\max$-expression, and no worse in the +others. To this end a new function, $P_{\max}: ((E_{\max} \to E), (X \to D)) \to (E_{\max} \to E)$, is used below as a ``strategy improvement -operator''. It takes a $\max$-strategy and a variable assignment and -returns a new $\max$-strategy which constitutes an `improvement' of -the strategy in the variable assignment $\rho$. - -In more precise terms, if have a $\max$-strategy $\sigma$, a variable -assignment $\rho$ and $\varsigma = P_{\max}(\sigma, \rho)$. Then: +operator''. $P_{\max}$ takes a $\max$-strategy and a variable +assignment and returns a new $\max$-strategy which constitutes an +`improvement' of the strategy in the variable assignment $\rho$. If +have a $\max$-strategy $\sigma$, a variable assignment $\rho$ and +$\varsigma = P_{\max}(\sigma, \rho)$. Then: \begin{align*} \sigma(\system)(\rho) \le \varsigma(\system)(\rho) \end{align*} @@ -438,13 +426,13 @@ the approach presented in Listing \ref{algo:naive-strategy}. \label{algo:naive-strategy} \end{algorithm} -This approach is quite similar to that of Kleene iteration, but from +This approach is quite similar to that of Kleene iteration, and from the results of Gawlitza et al.\cite{Gawlitza:2007:PFC:1762174.1762203} -it is known that this iteration is guaranteed to terminate. It is -still an inefficient way to solve this problem, however, for many of -the same reasons as Kleene iteration. It may spend significant time -attempting to improve strategies which can not have changed and thus -may perform a significant amount of unnecessary work. +it is known that this iteration is guaranteed to terminate. This naive +approach is an inefficient way to solve this problem, however, for +many of the same reasons as Kleene iteration. A large amount of time +will be spent attempting to improve portions of the strategy for which +no improvement can be made. \subsection{Adapted W-DFS algorithm} \label{sec:adapted-wdfs} @@ -529,51 +517,60 @@ some of the $\max$-expressions which may influence it are changed. For this particular algorithm to work, however, we must assume another property of $P_{\max}$. In Listing \ref{algo:adapted-wdfs} we take the -value of $P_{\max}(\lambda y . \eval(x, y), \rho)[x]$. That is: -improve the strategy, then use only the strategy for $x$. In order for -this algorithm to be correct $P_{\max}$ must always improve the -strategy at $x$ if it is possible to do so. +value of $P_{\max}(\lambda y . \eval(x, y), \rho)[x]$; we improve the +strategy, then use only the strategy for $x$. In order for this +algorithm to be correct $P_{\max}$ must always improve the strategy at +$x$ if it is possible to do so. If $P_{\max}$ did not improve the +strategy at $x$, while a permissible improvement existed, then we +would consider $x$ to be ``stable'' and would not attempt to improve +our strategy at $x$ until the improvement of another portion of our +strategy invalidated $x$. It is not guaranteed that another strategy +improvement will invalidate the strategy at $x$, however, so the +strategy at $x$ may still be able to be improved when the algorithm +terminates. If the strategy at $x$ can still be improved then we have +not reached the solution of our $\max$-strategy iteration. Additionally, in order to remain efficient, $P_{\max}$ should not attempt to improve the strategy for any $\max$-expressions until that -expression is requested. This will not affect the correctness of the -algorithm, but will significantly improve the performance of it. +expression is requested. Whether or not $P_{\max}$ is lazy in this way +will not affect the correctness of the algorithm, as it will only +result in the $\max$-strategy improvement at each step being more +expensive. The extra work to improve other portions of the strategy +will be discarded with only $P_{\max}(...)[x]$ being used. \section{Local Demand-driven Strategy Improvement (LDSI)} W-DFS can be used to speed up both the $\max$-strategy iteration and the fixpoint iteration as two independent processes, but each time we -seek to improve our strategy we must compute at least a subset of the -fixpoint from a base of no information. Ideally we would be able to -provide some channel for communication between the two W-DFS instances -to reduce the amount of work that must be done at each stage. By -supplying each other with information about which parts of the system -have changed we can jump in partway through the process of finding a -fixpoint, thereby avoiding repeating work that we have already done -when it is unnecessary to do so. +seek to improve our strategy we compute at least a subset of the +greatest fixpoint from a base of no information. We would like to be +able to provide some channel for communication between the two W-DFS +instances to reduce the amount of work that must be done at each +stage. By supplying each other with information about which parts of +the system have changed we can jump in partway through the process of +finding a fixpoint, thereby avoiding repeating work that we have +already done when it is unnecessary to do so. The new \emph{Local Demand-driven Strategy Improvement} algorithm, \emph{LDSI}, 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 can modify the fixpoint iteration algorithm to report which variables it has modified with -each fixpoint iteration step. - -This essentially results in a $\max$-strategy iteration which, at each -strategy-improvement step, invalidates a portion of the current -fixpoint iteration which may depend on the changed strategy. The -fixpoint iteration then re-stabilises each variable as it is -requested, tracking which values have changed since the last time they -were stabilised. The $\max$-strategy iteration then uses this list of -changed variables to determine which portions of the current strategy -must be re-stabilised once more. This process continues until the -$\max$-strategy stabilises (at which point the fixpoint will also -stabilise). +each fixpoint iteration step. We then have a $\max$-strategy iteration +which, at each strategy-improvement step, invalidates a portion of the +current fixpoint iteration which may depend on the changed +strategy. The fixpoint iteration then re-stabilises each variable as +it is requested, tracking which values have changed since the last +time they were stabilised. The $\max$-strategy iteration then uses +this list of changed variables to determine which portions of the +current strategy must be re-stabilised once more. This process +continues until the $\max$-strategy stabilises (at which point the +fixpoint will also stabilise). -This entire approach is \emph{demand driven}, and so any necessary -evaluation of strategies or fixpoint values is delayed until the point -when it is actually required. This means that the solver will be -\emph{local}. +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}). @@ -582,24 +579,30 @@ when it is actually required. This means that the solver will be This algorithm is presented in three parts. -Section \ref{sec:ldsi:top-level} presents the global state and entry -point to the algorithm. - -Section \ref{sec:ldsi:fixpoint} presents the fixpoint portion of -the algorithm. This portion bears many similarities to the W-DFS -algorithm presented in Section \ref{sec:wdfs}, with a few -modifications to track changes and allow external invalidations of -parts of the solution. - -Section \ref{sec:ldsi:max-strategy} presents the $\max$-strategy portion -of the algorithm. This portion is quite similar to the Adapted W-DFS -algorithm presented in Section \ref{sec:adapted-wdfs}, with some -modifications to allow for communication with the fixpoint portion of -the algorithm. - -Section \ref{sec:ldsi:correctness} argues the correctness of this -approach for finding the least fixpoints of monotonic, expansive -equation systems involving $\max$-expressions. +\begin{itemize} +\item + Section \ref{sec:ldsi:top-level} presents the global state and entry + point to the algorithm. + +\item + Section \ref{sec:ldsi:fixpoint} presents the fixpoint portion of the + algorithm. This portion bears many similarities to the W-DFS + algorithm presented in Section \ref{sec:wdfs}, with a few + modifications to track changes and allow external invalidations of + parts of the solution. + +\item + Section \ref{sec:ldsi:max-strategy} presents the $\max$-strategy + portion of the algorithm. This portion is quite similar to the + Adapted W-DFS algorithm presented in Section \ref{sec:adapted-wdfs}, + with some modifications to allow for communication with the fixpoint + portion of the algorithm. + +\item + Section \ref{sec:ldsi:correctness} argues the correctness of this + approach for finding the least fixpoints of monotonic, expansive + equation systems involving $\max$-expressions. +\end{itemize} \subsection{Top level} \label{sec:ldsi:top-level} @@ -680,14 +683,11 @@ functions presented in Sections \ref{sec:wdfs} and also initialised, as they was not present in either of the previous $\init$ functions. -It is important to note, also, that $D$ and $D_\old$ are both -initialised to \underline{$-\infty$} and $\stableFP$ is initially the -entire set of variables. This is because we are beginning with a known -strategy mapping every max expression to $-\infty$, so we already know -that each fixpoint value must be stable at $-\infty$, so we can save -an entire fixpoint iteration step by taking this into account. This -state corresponds to an already complete fixpoint iteration with the -given initial strategy. +$D$ and $D_\old$ are both initialised to \underline{$-\infty$} and +$\stableFP$ is initially the entire set of variables. The values of +$D$, $D_\old$ and $\stableFP$ are set to their result after a complete +fixpoint iteration over each variable with the initial +$\max$-strategy. The type of this function is also different to either of the original $\init$ functions. $\init : \Systems \to (X \to \CZ)$. The function @@ -701,12 +701,12 @@ each variable for the least fixpoint, returning a value in $\CZ$. The process of fixpoint iteration is extremely similar to the fixpoint iteration algorithm presented in Section \ref{sec:wdfs}. The only -difference is that we have an $\invalidate \fixpoint$ procedure which -allows the $\max$-strategy iteration to invalidate a portion of the -system to ensure its value is recalculated by the fixpoint iteration -process. The last stable value is also stored in this procedure to -allow \emph{changed} values to be identified, not merely -\emph{invalidated} ones. +difference is that we have an $\invalidate \fixpoint$ procedure for +the $\max$-strategy iteration to invalidate a portion of the +system. By invalidating only a portion of the system we reuse the +values which have already been computed to avoid performing additional +work. The last stable value is also stored in this procedure to +identify \emph{changed} values, rather than only \emph{unstable} ones. \begin{algorithm}[H] \begin{algorithmic} @@ -722,12 +722,10 @@ allow \emph{changed} values to be identified, not merely \label{algo:ldsi:fixpoint:eval} \end{algorithm} -This procedure is exactly the same as the equivalent method in the -W-DFS algorithm, except for the fact that $\solve$ has been renamed to -$\solve \fixpoint$. It allows us to track dependencies between -fixpoint variables by injecting this function as our variable-lookup -function. It then both calculates a new value for the variable (the -$\solve \fixpoint$ call) and notes the dependency between $x$ and $y$. +This procedure is similar to the equivalent method in the W-DFS +algorithm, except for the fact that $\solve$ has been renamed to +$\solve \fixpoint$. $\eval \fixpoint$ performs exactly the same +function as the $\eval$ function in Figure \ref{algo:wdfs}. \begin{algorithm}[H] \begin{algorithmic} @@ -753,11 +751,13 @@ $\solve \fixpoint$ call) and notes the dependency between $x$ and $y$. This procedure is not called in the fixpoint iteration process, but is rather the method by which the $\max$-strategy iteration can -communicate with the fixpoint-iteration. It allows the $\max$-strategy -iteration to inform the fixpoint-iteration which values have changed -and will require re-evaluation. This makes it possible to only -re-evaluate a partial system (the solving of which is also be delayed -until requested by the $\solve \fixpoint$ procedure). +communicate with the fixpoint-iteration. A call to $\invalidate +\fixpoint$ indicates to the fixpoint-iteration that a variable's value +\emph{may} have changed as a result of a $\max$-strategy improvement, +and that it will require re-calculation. The invalidation provided by +this procedure permits us to only re-evaluate a partial system (the +solving of which is also be delayed until requested by the $\solve +\fixpoint$ procedure). While invalidating variables we also note their $\old$ value, and mark them as ``touched''. As the $\old$ value is only set in this @@ -794,13 +794,13 @@ us from doing extra work in the $\max$-strategy iteration phase. The $\solve \fixpoint$ procedure is extremely similar to the $\solve$ procedure presented in Listing \ref{algo:wdfs}. There are two main -differences: the self-recursive call has been renamed (to reflect the -change in the function's name), and instead of using $\system[x]$ we -must use $\sigma(\system[x])$. The use of $\sigma$ is to ensure that -the fixpoint is solving the variable using the current -$\max$-strategy. This $\max$-strategy is stable for the duration of -the $\solve \fixpoint$ execution, so it will result in fixpoint -iteration being performed over a stable system. +differences: the self-recursive call has been renamed to reflect the +change in the function's name, and instead of using $\system[x]$ we +must use $\sigma(\system[x])$. We use $\sigma$ to provide the +fixpoint-iteration with the current $\max$-strategy. $\sigma$ is +stable for the duration of the $\solve \fixpoint$ execution, so it +will result in fixpoint iteration being performed over a stable +system. After an evaluation of the $\solve \fixpoint$ procedure, the variable $x$ will have its value in the current $\max$-strategy's greatest |