diff options
Diffstat (limited to 'tex/thesis')
| -rw-r--r-- | tex/thesis/contribution/contribution.tex | 205 |
1 files changed, 145 insertions, 60 deletions
diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex index b5d47db..44e5e7d 100644 --- a/tex/thesis/contribution/contribution.tex +++ b/tex/thesis/contribution/contribution.tex @@ -10,12 +10,15 @@ \newcommand\system{\mathcal{E}} %\mathsf{system}} \newcommand\parent{\mathsf{parent}} \newcommand\parents{\mathsf{parents}} +\newcommand\val{\mathsf{val}} \newcommand\old{\mathsf{old}} +\newcommand\best{\mathsf{best}} +\newcommand\all{\mathsf{all}} \newcommand\Operators{\mathcal{O}} \newcommand\Systems{\varepsilon} - +\newcommand\improve{\mathsf{\textsc{improve}}} \newcommand\init{\mathsf{\textsc{init}}} \newcommand\eval{\mathsf{\textsc{eval}}} \newcommand\stabilise{\mathsf{\textsc{stabilise}}} @@ -24,8 +27,9 @@ \newcommand\fixpoint{\mathsf{\textsc{fixpoint}}} \newcommand\strategy{\mathsf{\textsc{strategy}}} -\algblockx[Globals]{Globals}{EndGlobals}{\textbf{Globals:\\}}{} -\algblockx[Assume]{Assumptions}{EndAssumptions}{\textbf{Assume:\\}}{} +\algblockx[Globals]{Globals}{EndGlobals}{\textbf{Globals:\\}}{} +\algblockx[Assume]{Assumptions}{EndAssumptions}{\textbf{Assume:\\}}{} +\algblockdefx[ReturnLambdaFn]{ReturnLambdaFn}{EndReturnLambdaFn}[1]{\textbf{return function} (#1)}{\textbf{end function}} \chapter{Contribution} \label{chap:contribution} @@ -92,21 +96,25 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$. : (X \to \CZ) \to \CZ$, a mapping from a variable assignment to the expression's value in that assignment. - Expressions have two possible forms: + Expressions have three possible forms: \begin{itemize} - \item $e = f( e_1, e_2, ..., e_k )$, with $f: \CZ^k \to \CZ$ and + \item + $e = f( e_1, e_2, ..., e_k )$, \\ + with $f: \CZ^k \to \CZ$ and $e_1, e_2, ... e_k \in E$ and $e(\rho) = f(e_1(\rho), - e_2(\rho), ..., e_k(\rho))$. - \item $e = x \in X$, with $e(\rho) = \rho(v)$ + e_2(\rho), ..., e_k(\rho))$ + \item $e = x \in X$, with $e(\rho) = \rho(x)$ + \item $e = z \in \CZ$, with $e(\rho) = z$ \end{itemize} The subset of expressions of the form $\max\{ e_1, e_2, ... e_k \}$, with $e_1, e_2, ..., e_k \in E$ are referred to as \emph{$\max$-expressions}, denoted by $E_{\max} \subset E$. - For an expression $e$, the set of expressions containing it, $\{ - e_\parent \mid e_\parent = o\{ e_1, e_2, ... e_k \}, o \in \O, e_i - \in E \}$, is denoted $\parents(e)$. + We define a function $\parents: E \to 2^E$, taking an expression, + $e$, to the set of expressions containing $e$, $\{ e_\parent \mid + e_\parent = f\{ ..., e, ... \}, f: \CZ^k \to \CZ \}$. $e$ is then + said to be a \emph{subexpression} of $e_{\parent}$. \end{definition} \begin{definition} @@ -135,8 +143,8 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$. We define an inverse mapping, $\system^{-1} : E \to 2^X$, taking an expression, $e$, to the set of variables, $x$ for which it is a - ``subexpression'' of $\system[x]$. This is captured in the following - definition: + transitive subexpression of $\system[x]$. This is captured in the + following definition: \begin{align*} \system^{-1}(e) &= \{ x \mid system(x) = e \} \cup \{ \system^{-1}(e_\parent) \mid e_\parent \in parents(e) \} @@ -317,16 +325,46 @@ The W-DFS algorithm provides us with a \emph{local}, fixpoint problems. \begin{figure}[H] - \begin{align*} - x &= \min(0, y) \\ - y &= x \\ - a &= \min(0, b) \\ - b &= c \\ - c &= d \\ - d &= e \\ - e &= a \ - \end{align*} - \caption{Example equation system for a W-DFS solve} + \begin{tikzpicture} + \node[draw] (full) at (0,-2) { + \begin{minipage}{0.3\textwidth} + \begin{align*} + x &= \min(0, y) \\ + y &= x \\ + a &= \min(0, b) \\ + b &= c \\ + c &= d \\ + d &= e \\ + e &= a + \end{align*} + \end{minipage} + }; + + \node[draw] (first) at (10, 1) { + \begin{minipage}{0.3\textwidth} + \begin{align*} + x &= \min(0, y) \\ + y &= x + \end{align*} + \end{minipage} + }; + \node[draw] (second) at (10,-4) { + \begin{minipage}{0.3\textwidth} + \begin{align*} + a &= \min(0, b) \\ + b &= c \\ + c &= d \\ + d &= e \\ + e &= a + \end{align*} + \end{minipage} + }; + + \draw[->] (full) -- (first); + \draw[->] (full) -- (second); + \end{tikzpicture} + \caption{Example of an equation system which can be separated into + two independent sub-systems} \label{fig:wdfs-example} \end{figure} @@ -336,14 +374,14 @@ 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. +value of a variable in either of these subsystems it is necessary to +evaluate the entire subsystem, but it is not necessary to evaluate the +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 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 @@ -360,9 +398,11 @@ greatest-fixpoint problems. 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 use $\sigma: \Systems \to \Systems$ as a +subexpression. 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)$. Similarly +$\sigma_{\all}: E \to E$ will denote the expression obtained by +replacing each $\max$-subexpression in $e$ with $\sigma(e)$. In the particular case of \emph{monotonic}, \emph{expansive} operators it has been shown\cite{Gawlitza:2007:PFC:1762174.1762203} that this @@ -372,19 +412,45 @@ strategy. This means that each time we improve our strategy we must 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) \times (X \to D)) -\to (E_{\max} \to E)$, is used below as a ``strategy improvement -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: +To this end a new function, $\improve: ((E_{\max} \to E) \times +(X \to D)) \to (E_{\max} \to E)$, is used below as a \emph{strategy + improvement operator}. $\improve$ 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 = \improve(\sigma, +\rho)$. Then: \begin{align*} \sigma(\system)(\rho) \le \varsigma(\system)(\rho) \end{align*} -If it is possible for $\sigma$ to be improved then $P_{\max}$ will -return an improvement, otherwise it will return $\sigma$ unchanged. +If it is possible for $\sigma$ to be improved then $\improve$ will +return an improvement, otherwise it will return $\sigma$ +unchanged. One possible implementation of $\improve$ is presented in +Listing \ref{algo:pmax}. It will try every option of subexpressions +for this $\max$-expression and will then return the best. The use of +an anonymous function as the returned strategy is so the evaluation of +each strategy is only done when requested. + +\begin{algorithm} + \begin{algorithmic} + \Function {improve} {$\sigma: E_{\max} \to E$, $\rho: X \to D$} + \ReturnLambdaFn {$e \in E_{\max}$} + \State $e_{\best} = \sigma(e)$ + \State $\val_{\best} = \sigma_{\all}(e_{\old})(\rho)$ + \For {$e_i \in e$} + \If {$\sigma_{\all}(e_i)(\rho) > \val_{\best}$} + \State $e_{\best} = e_i$ + \State $\val_{\best} = \sigma(e_i)(\rho)$ + \EndIf + \EndFor + \State \Return $e_{\best}$ + \EndReturnLambdaFn + \EndFunction + \end{algorithmic} + \caption{The variation of $\improve$ used in our algorithm} + \label{algo:pmax} +\end{algorithm} \subsection{Naive approach} @@ -405,7 +471,7 @@ the approach presented in Listing \ref{algo:naive-strategy}. $\rho$ & $: X \to D$, a variable assignment \\ - $P_{\max}$ & $: ((E_{\max} \to E) \times (X \to \CZ)) \to (E_{\max} + $\improve$ & $: ((E_{\max} \to E) \times (X \to \CZ)) \to (E_{\max} \to E)$, a $\max$-strategy improvement operator \\ \end{tabularx} \EndAssumptions @@ -415,7 +481,7 @@ the approach presented in Listing \ref{algo:naive-strategy}. \State $\sigma_0 = \{ x \mapsto -\infty \mid \forall x \in X \}$ \State $\rho_0 = \underline{-\infty}$ \Repeat - \State $\sigma_{k+1} = P_{\max}(\sigma_k, \rho_k)$ + \State $\sigma_{k+1} = \improve(\sigma_k, \rho_k)$ \State $\rho_{k+1} = \solve \fixpoint(\sigma_{k+1}(\system))$ \State $k = k + 1$ \Until {$\sigma_{k-1} = \sigma_k$} @@ -454,14 +520,14 @@ solve $\max$-strategy iteration problems. $\max$-expressions to a subexpression \\ $\inflSI$ & $: (E_{\max} \to 2^{E_{\max}}$, a mapping from a - $\max$-expression to the sub-expressions it influences \\ + $\max$-expression to the subexpressions it influences \\ $\stableSI$ & $\subseteq E_{\max}$, the set of all $\max$-expressions whose strategies are stable \\ $\system$ & $\in \Systems$, an equation system \\ - $P_{\max}$ & $: ((E_{\max} \to E) \times (X \to \CZ)) \to (E_{\max} + $\improve$ & $: ((E_{\max} \to E) \times (X \to \CZ)) \to (E_{\max} \to E)$, a $\max$-strategy improvement operator \\ \end{tabularx} \EndGlobals @@ -491,7 +557,7 @@ solve $\max$-strategy iteration problems. \If {$x \not \in \stableSI$} \State $\stableSI = \stableSI \cup \{x\}$ \State $\rho = \solve \fixpoint(\sigma(\system))$ - \State $v = P_{\max}(\lambda y . \eval(x, y), \rho)[x]$ + \State $v = \improve(\lambda y . \eval(x, y), \rho)[x]$ \If {$v \ne \sigma[x]$} \State $\sigma = \{ x \mapsto v\} \oplus \sigma$ \State $W = \inflSI[x]$ @@ -516,11 +582,11 @@ only attempt to improve the strategy for a given $\max$-expression if 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]$; we improve the +property of $\improve$. In Listing \ref{algo:adapted-wdfs} we take the +value of $\improve(\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 +algorithm to be correct $\improve$ must always improve the strategy at +$x$ if it is possible to do so. If $\improve$ 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 @@ -528,15 +594,20 @@ 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. +not reached the solution of our $\max$-strategy iteration. The +particular $\improve$ that we are using (see Listing \ref{algo:pmax}) +satisfies this assumption, as it attempts to improve the strategy at +the point of individual $\max$-expressions. -Additionally, in order to remain efficient, $P_{\max}$ should not +Additionally, in order to remain efficient, $\improve$ should not attempt to improve the strategy for any $\max$-expressions until that -expression is requested. Whether or not $P_{\max}$ is lazy in this way +expression is requested. Whether or not $\improve$ 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. +will be discarded with only $\improve(...)[x]$ being used. The +particular $\improve$ that we are using (see Listing \ref{algo:pmax}) +satisfies this property by way of its anonymous function. \section{Local Demand-driven Strategy Improvement (LDSI)} @@ -631,12 +702,12 @@ This algorithm is presented in three parts. $\max$-expressions to a subexpression \\ $\inflSI$ & $: E_{\max} \to 2^{E_{\max}}$, a mapping from a - $\max$-expression to the sub-expressions it influences \\ + $\max$-expression to the subexpressions it influences \\ $\stableSI$ & $\subseteq E_{\max}$, the set of all $\max$-expressions whose strategies are stable \\ - $P_{\max}$ & $: ((E_{\max} \to E) \times (X \to \CZ)) \to + $\improve$ & $: ((E_{\max} \to E) \times (X \to \CZ)) \to (E_{\max} \to E)$, a $\max$-strategy improvement operator \\ \\ @@ -892,14 +963,16 @@ themselves destabilised as well. \Procedure {solvestrategy} {$x \in E_{\max}$} \If {$x \not \in \stableSI$} \State $\stableSI = \stableSI_{\max} \cup \{x\}$ - \State $e = P_{\max}(\lambda y . \eval \strategy(x,y), - \lambda y . \eval \strategy \fixpoint(x, y))[x]$ + \State $e = \improve(\lambda y . \eval \strategy(x,y), + \lambda z . \eval \strategy \fixpoint(x, z))[x]$ \If {$e \ne \sigma[x]$} \State $\sigma = \{ x \mapsto e \} \oplus \sigma$ - \State $\invalidate \fixpoint(\system^{-1}(x))$ + \For {$v \in \system^{-1}(x)$} + \State $\invalidate \fixpoint(\system^{-1}(x))$ + \EndFor \State $\stableSI = \stableSI \backslash I[x]$ \For {$v \in \inflSI[x]$} - \State $\solve(v)$ + \State $\solve \strategy(v)$ \EndFor \EndIf \EndIf @@ -911,8 +984,18 @@ themselves destabilised as well. + + \subsection{Correctness} \label{sec:ldsi:correctness} +To argue the correctness of our LDSI algorithm we will first establish +some invariants, after which it should be much easier to see why our +algorithm is correct. + +%\begin{invariant} +First of all $\fixpoint \solve$. +%\end{invariant} + In order to argue that LDSI is correct we must first assume that the W-DFS algorithm of Seidl et al.~is correct and will solve the equation system for its least/greatest fixpoint. @@ -938,3 +1021,5 @@ The strategy-iteration step invalidates anything that \emph{might} depend on $\system[x]$ while it invalidates $x$, thereby ensuring that any further calls to $\solve \strategy$ will result in a correct value for the given strategy. + +\subsection{Implementation} \label{sec:ldsi:implementation} |