summaryrefslogtreecommitdiff
path: root/tex/thesis
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis')
-rw-r--r--tex/thesis/contribution/contribution.tex205
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}