From cd087d4597ec8119f8a25271797589db15c25b9e Mon Sep 17 00:00:00 2001
From: Carlo Zancanaro <carlo@carlo-laptop>
Date: Mon, 19 Nov 2012 10:34:25 +1100
Subject: Thesis stuff. Contribution & lit review.
---
tex/thesis/contribution/contribution.tex | 360 +++++++++++++++++++------------
tex/thesis/litreview/litreview.tex | 67 +++++-
tex/thesis/references.bib | 11 +
tex/thesis/thesis.tex | 1 +
4 files changed, 301 insertions(+), 138 deletions(-)
diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index 44e5e7d..e41a39f 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -1,9 +1,11 @@
\floatname{algorithm}{Listing}
\newcommand\inflFP{\mathsf{infl^{FP}}}
+\newcommand\depFP{\mathsf{dep^{FP}}}
\newcommand\stableFP{\mathsf{stable^{FP}}}
\newcommand\touchedFP{\mathsf{touched^{FP}}}
\newcommand\inflSI{\mathsf{infl^{SI}}}
+\newcommand\depSI{\mathsf{dep^{SI}}}
\newcommand\stableSI{\mathsf{stable^{SI}}}
\newcommand\stable{\mathsf{stable}}
@@ -15,8 +17,14 @@
\newcommand\best{\mathsf{best}}
\newcommand\all{\mathsf{all}}
+\newcommand\fix{\mathsf{fix}}
+\newcommand\soln{\mathsf{soln}}
+
+\newcommand\post{\mathsf{post}}
+\newcommand\pre{\mathsf{pre}}
+
\newcommand\Operators{\mathcal{O}}
-\newcommand\Systems{\varepsilon}
+\newcommand\Systems{\mathbb{E}}
\newcommand\improve{\mathsf{\textsc{improve}}}
\newcommand\init{\mathsf{\textsc{init}}}
@@ -32,7 +40,7 @@
\algblockdefx[ReturnLambdaFn]{ReturnLambdaFn}{EndReturnLambdaFn}[1]{\textbf{return function} (#1)}{\textbf{end function}}
-\chapter{Contribution} \label{chap:contribution}
+\chapter{Demand-driven strategy improvement} \label{chap:contribution}
In this chapter the main theoretical contribution of this thesis is
presented: an extension on a $\max$-strategy iteration algorithm for
@@ -56,14 +64,10 @@ operations consists of naively ``evaluating'' the system repeatedly
until a further evaluation results in no change. Gawlitza et
al.~proved that these iterations must converge in a finite number of
steps\cite{Gawlitza:2007:PFC:1762174.1762203} , but in practice this
-naive approach performs many more operations than are necessary, in
-many cases re-calculating results which are already known.
+naive approach performs a large number of re-calculations of results
+which are already known.
% TODO: add something here about variable dependencies
-%By considering which variables depend on, and influence, each other it
-%is possible to reduce the amount of work that is to be done quite
-%considerably.
-
\section{Preliminaries}
In order to aid our explanation of these algorithms we will now define
@@ -71,41 +75,48 @@ a few terms and notations. We will assume a fixed, finite set $X$ of
variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$.
\begin{definition}
- A \textbf{Variable Assignment} is a partial function, $\rho: X \to
- \CZ$, from a variable to a value. The domain of a variable
+ A \textbf{variable assignment} is a partial function, $\rho: X \to
+ \CZ$ that maps variables to values. The domain of a variable
assignment, $\rho$, is represented by $\mathsf{domain}(\rho)
- \subseteq X$.
-
- An underlined value, $\underline{a}$ indicates a variable assignment
- $\{ x \mapsto a \mid \forall x \in X \}$.
-
- Variable assignments $\rho \in X \to \CZ$ and $\varrho \in X \to
- \CZ$ may be composed with the $\oplus$ operator in the following
- way:
+ \subseteq X$. An underlined value, $\underline{a}$, indicates a
+ variable assignment $\{ x \mapsto a \mid \forall x \in X \}$.
+ Variable assignments $\rho : X \to \CZ$ and $\varrho : X \to \CZ$
+ may be composed with the $\oplus$ operator in the following way:
\begin{align*}
- \rho \oplus \varrho = \left\{\begin{array}{lc}
+ (\rho \oplus \varrho)(x) = \left\{\begin{array}{lc}
\varrho(x) & x \in \mathsf{domain}(\varrho) \\
\rho(x) & \mbox{otherwise}
- \end{array}\right.
+ \end{array}\right., \forall x \in X
\end{align*}
\end{definition}
\begin{definition}
- \textbf{Expressions:} We will consider expressions, $e \in E$, as $e
- : (X \to \CZ) \to \CZ$, a mapping from a variable assignment to the
- expression's value in that assignment.
+ \textbf{Expressions:}
- Expressions have three possible forms:
+ The class of expressions, $E$, is defined inductively:
\begin{itemize}
\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(x)$
- \item $e = z \in \CZ$, with $e(\rho) = z$
+ If $z \in \CZ$ then $z \in E$
+ \item
+ If $x \in X$ then $x \in E$
+ \item
+ If $f : \CZ^k \to \CZ$ and $e_1,...,e_k \in E$ then
+ $f(e_1,...,e_k) \in E$
+ \item
+ Nothing else is in E.
\end{itemize}
+
+ We then define the semantics of these expressions by:
+ \begin{align*}
+ \llb z \rrb &= \lambda \rho . z & \forall z \in \CZ \\
+ \llb x \rrb &= \lambda \rho . \rho(x) & \forall x \in X \\
+ \llb f(e_1,...,e_k) \rrb &=
+ \lambda \rho . f(\llb e_1 \rrb(\rho),...,\llb e_k \rrb(\rho))
+ \end{align*}
+
+ By abusing our notation we will consider expressions, $e \in E$, as
+ $e : (X \to \CZ) \to \CZ$ defined by $e = \llb e \rrb$.
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
@@ -119,16 +130,20 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$.
\begin{definition}
\textbf{Equation System:} An equation system is a mapping from
- variables to expressions. $\system : X \to E_\system$, where
- $E_\system \subset E$. As each element of $E$ is also a function $(X
- \to \CZ) \to \CZ$, so an equation system can be considered as a
- function $\system : X \to ((X \to \CZ) \to \CZ)$ (which is
- equivalent to the above).
+ variables to expressions. $\system : X \to E$. We define
+ $E_\system \subset E$ to be the preimage of system, that is
+ $E_\system = \{ e \in E \mid system(x) = e, \forall x \in X \}$. As
+ each element of $E$ is also a function $(X \to \CZ) \to \CZ$, so an
+ equation system is considered as a function $\system : X \to
+ ((X \to \CZ) \to \CZ)$ (which is equivalent to the above).
Alternatively an equation system can be represented as a function
$\system : (X \to \CZ) \to (X \to \CZ)$, $\system(\rho)[x] =
e_x(\rho)$, taking a variable assignment $\rho$ and returning the
- result of each $e_x$'s evaluation in $\rho$.
+ result of each $e_x$'s evaluation in $\rho$. We use this second form
+ as a convenience for when we are evaluating the entire equation
+ system in the context of a variable assignment: we get a new value
+ for each variable and thus a new variable assignment as a result.
These two functional forms are equivalent and correspond to changing
the argument order in the following way: $\system(\rho)[x] =
@@ -192,7 +207,7 @@ algorithm is presented in Listing \ref{algo:kleene}.
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
+approach which evaluates smaller portions of the system in each
iteration would be a significant improvement.
An additional deficiency of Kleene iteration is that it is not
@@ -215,20 +230,20 @@ x \mapsto -\infty, y \mapsto -\infty \}$.
\label{fig:kleene-infinite}
\end{figure}
-This particular non-termination of Kleene iteration is not a
-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|^3)$ right hand side evaluations, which is
-very inefficient.
+It has been shown by Gawlitza et
+al.\cite{Gawlitza:2007:PFC:1762174.1762203} that Kleene iteration is
+at most restricted to $|X|$ iterations in the particular case of the
+$\max$-strategy iteration algorithm considered in this thesis. Kleene
+iteration is therefore restricted to $\Theta(|X|^3)$ right hand side
+evaluations at most in our application. We seek to improve on this
+performance in the next section.
\subsection{W-DFS algorithm} \label{sec: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
+dependencies we can leave portions of the system unevaluated when we
+are certain that those values have not changed. The algorithm is
presented in Listing \ref{algo:wdfs}.
\begin{algorithm}
@@ -302,9 +317,9 @@ 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
+value is requested, whether externally or internally. Once a value is
requested the right-hand-side is evaluated, which may in turn request
-the values of other variables (through the $\eval$ function).
+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 is calculated we
@@ -360,8 +375,8 @@ fixpoint problems.
\end{minipage}
};
- \draw[->] (full) -- (first);
- \draw[->] (full) -- (second);
+ \draw (full) -- (first.west);
+ \draw (full) -- (second.west);
\end{tikzpicture}
\caption{Example of an equation system which can be separated into
two independent sub-systems}
@@ -412,25 +427,25 @@ 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, $\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:
+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 $\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.
+If there is a possible improvement to be made on $\sigma$ then
+$\improve$ will return an improvement, otherwise it will return
+$\sigma$ unchanged. One possible implementation of $\improve$ is
+presented in Listing \ref{algo:pmax}. This implementation 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}
@@ -495,10 +510,9 @@ the approach presented in Listing \ref{algo:naive-strategy}.
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. 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.
+approach is inefficient, however, in the same way 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}
@@ -576,10 +590,11 @@ solve $\max$-strategy iteration problems.
\end{algorithm}
This approach retains the benefits of the W-DFS algorithm for solving
-fixpoints, but applies them to $\max$-strategy iteration problems. It
-will take into account dependencies between the $\max$-expressions and
-only attempt to improve the strategy for a given $\max$-expression if
-some of the $\max$-expressions which may influence it are changed.
+fixpoints, but applies them to $\max$-strategy iteration
+problems. Dependencies between $\max$-expressions are considered and
+an improvement on the strategy at an expression $e$ is only attempted
+if some of the $\max$-expressions which influence $e$ themselves
+improve strategy.
For this particular algorithm to work, however, we must assume another
property of $\improve$. In Listing \ref{algo:adapted-wdfs} we take the
@@ -611,16 +626,16 @@ satisfies this property by way of its anonymous function.
\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 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.
+W-DFS speeds up both the $\max$-strategy iteration and the fixpoint
+iteration as two independent processes, but each time we 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
@@ -760,7 +775,7 @@ $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
+The type of this function is different to either of the original
$\init$ functions. $\init : \Systems \to (X \to \CZ)$. The function
returned by $\init$ performs the entire process of $\max$-strategy
iteration and fixpoint iteration and calculates the final value of
@@ -770,14 +785,14 @@ each variable for the least fixpoint, returning a value in $\CZ$.
\subsection{Fixpoint iteration} \label{sec:ldsi:fixpoint}
-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 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.
+The process of fixpoint iteration is similar to the fixpoint iteration
+algorithm presented in Section \ref{sec:wdfs}. The only 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 stored in this procedure to identify
+\emph{changed} values, rather than only \emph{unstable} ones.
\begin{algorithm}[H]
\begin{algorithmic}
@@ -795,8 +810,8 @@ identify \emph{changed} values, rather than only \emph{unstable} ones.
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 Listing \ref{algo:wdfs}.
+$\solve \fixpoint$. $\eval \fixpoint$ performs the same function as
+the $\eval$ function in Listing \ref{algo:wdfs}.
\begin{algorithm}[H]
\begin{algorithmic}
@@ -827,15 +842,15 @@ communicate with the fixpoint-iteration. A call to $\invalidate
\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).
+solving of which is delayed until requested by the $\solve \fixpoint$
+procedure).
-While invalidating variables we also note their $\old$ value, and mark
+While invalidating variables we store their $\old$ value, and mark
them as ``touched''. As the $\old$ value is only set in this
procedure, and only when $x$ is stable, it gives us the ability to see
whether a variable has stabilised to a new value, or whether it has
-merely re-stabilised to the same value as last time. This can prevent
-us from doing extra work in the $\max$-strategy iteration phase.
+merely re-stabilised to the same value as last time. This refines the
+set of changed variables for the $\max$-strategy iteration phase.
@@ -863,11 +878,11 @@ us from doing extra work in the $\max$-strategy iteration phase.
\label{algo:ldsi:fixpoint:solve}
\end{algorithm}
-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])$. We use $\sigma$ to provide the
+The $\solve \fixpoint$ procedure is 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])$. 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
@@ -901,9 +916,9 @@ being stabilised.
\For {$w \in \inflSI[\strategy(\system[v])]$}
\State $\invalidate \strategy(\system[v])$
\EndFor
+ \State $\touchedFP = \touchedFP \backslash \{v\}$
\EndIf
\EndFor
-
\State \Return $D[y]$
\EndFunction
\end{algorithmic}
@@ -988,38 +1003,115 @@ 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.
-
-
-
+To argue the correctness of our LDSI algorithm we will first argue the
+correctness of the fixpoint iteration portion of the algorithm. We
+will then argue the correctness of the $\max$-strategy iteration
+portion, including the communication between the fixpoint iteration
+and $\max$-strategy iteration.
+
+
+The fixpoint iteration portion of the algorithm is concerned with
+finding the greatest fixpoint, $\soln(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 $\soln(s) \in \fix(s)$
+and $\soln(s) \ge \rho ~ \forall \rho \in \fix(s)$. Our general
+approach will be to consider our variable assignment $D \ge \soln(s)$
+and show that it decreases until $D \in \fix(s)$ and thus $D =
+\soln(s)$.
+
+We begin by stating two invariants of the LDSI algorithm. The set
+$\depFP^{+}(x)$ is the set of all variables which $x$ may depend
+on. $\depFP^{+}$ is defined as the transitive closure of $\depFP$,
+which is defined by $\depFP(x) = \{ y \in X \mid x \in \inflFP(y)
+\}$. $R \subseteq X$ is defined as the variables currently on our
+recursion stack.
+\begin{align}
+ D &\ge \soln(s) \label{eqn:fp-inv1} \\
+%
+ D &= \soln(s)[x] & \mbox{if }
+ x \in \stableFP,
+ x \not \in R,
+ \depFP^{+}(x) \cap R = \emptyset
+ \label{eqn:fp-inv2} \\
+%
+ x \in \inflFP[y] & \forall x \in \stableFP, y \in \depFP(x)
+ \label{eqn:fp-inv3}
+\end{align}
+
+(\ref{eqn:fp-inv1}) follows from monotonicity. We begin our iteration
+at some variable assignment $D \ge \soln(s)$ and monotonically descend
+from there. Each evaluation of a variable remains greater than
+$\soln(s)[x]$ because our variable assignment $D$ always satisfies $D
+\ge soln(s)$. We cannot jump below the greatest fixpoint because to do
+so would imply that we could ``turn around'' for at least one
+variable, thereby breaking our monotonicity assumption.
+
+For (\ref{eqn:fp-inv2}) we will examine what has happened when each of
+the conditions is false:
+\begin{itemize}
+\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. In either case, the value of $D[x]$ will be decreased, given
+ the value of the other variables in $X \backslash {x}$. 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}$.
-This algorithm relies on the correctness of the underlying W-DFS
-algorithm. This algorithm was presented in
-\cite{DBLP:tr/trier/MI96-11}.
+\item
+ If $\depFP^{+}(x) \cap R \ne \emptyset$ then a variable which $x$
+ depends on is in $R$ at the moment. This will result in the
+ re-evaluation of $x$ if the value of any of the variables in
+ $\depFP^{+}(x) \cap R$ have changed.
-If we assume that W-DFS is correct then we only have to prove that the
-combination algorithm is correct. For this it is sufficient to show
-that the invalidate calls in both directions preserve the correctness
-of the original algorithm.
+\item
+ If $x \in R$ 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 previous condition, that $x$ will
+ be entirely re-evaluated at some point after this one.
+\end{itemize}
-The fixpoint iteration step invalidates anything that \emph{might}
-depend on $x$ while it invalidates $x$, thereby ensuring that any
-further calls to $\solve \fixpoint$ will result in a correct value for
-the given strategy.
+(\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.
+
+After an evaluation of $\solve \fixpoint(x)$ we know that $x \in
+\solve \fixpoint(x)$. If it is also the case that $R = \emptyset$, as
+is the case for top-level calls to $\solve \fixpoint$, then we know
+that $D[x] = \soln(s)[x]$. This means that a 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 are maintained by this process.
+
+When the $\max$-strategy iteration portion invalidates a part of the
+fixpoint iteration it does 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) \}$,
+or $\{ 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}) and
+(\ref{eqn:fp-inv2}) hold for the entire subsystem which is affected by
+the change in strategy, and thus that our invariants hold for our
+entire system.
+
+This is sufficient for us to be confident that the fixpoint iteration
+portion of the algorithm is correct. The invariants ensure that $D$ is
+approaching $\soln(s)$ and we know that our invariants are maintained
+by the $\max$-strategy invalidating the fixpoint iteration.
+
+
+
+We move now to the $\max$-strategy iteration.
+% TODO: finish the proof
-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}
diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex
index 4b9f3da..bde7160 100644
--- a/tex/thesis/litreview/litreview.tex
+++ b/tex/thesis/litreview/litreview.tex
@@ -1,6 +1,7 @@
\newcommand{\Env}{\mathsf{Env}}
\newcommand{\PP}{\mathsf{PP}}
\newcommand{\States}{\mathsf{States}}
+\newcommand{\state}{\mathsf{state}}
\chapter{Literature Review} \label{chap:litreview}
@@ -8,7 +9,65 @@
In order to perform any static analysis of a program it is necessary
to have some notion of the \emph{semantics}, or meaning, of a
-program.
+program. The semantics of a program can be captured in several ways,
+but for our purposes we will consider Denotational
+Semantics\cite{SCOTT70B}.
+
+Denotational semantics takes a view of a program as a (partial)
+function built up by the composition of many smaller functions. By
+expressing our expressions, assignments, conditionals and loops as
+smaller functions we can then compose them to determine the semantics
+of our whole program. For imperative languages we consider each
+assignment, conditional or loop as having the denotation $\llb s \rrb:
+\state \to \state$. We define their composition as $\llb s_1 ; s_2
+\rrb = \llb s_2 \rrb \circ \llb s_1 \rrb$.
+
+As an example, we'll define some denotational semantics for a simple
+language. Here our $\state$ will be a partial function $\state: I \to N$
+\newcommand\halfpage[1]{\begin{minipage}{0.45\textwidth}#1\end{minipage}}
+\newcommand\halfpages[2]{\halfpage{#1}\hfill\halfpage{#2}}
+\begin{figure}[here]
+ \halfpages{Syntax:}{Semantics:}
+
+ \halfpages{
+ $P :: S$
+ }{
+ $P: \state \to \state$ \\
+ $P\llb S \rrb = S\llb S \rrb \{\}$
+ }
+ \halfpages{
+ $S ::= S_1;S_2 \mid if ~B~ then ~S_1~ else ~S_2~ \mid I := E$
+ }{
+ $S: \state \to \state$ \\
+ $S\llb S_1;S_2 \rrb = \lambda v . (S\llb S_2 \rrb (S\llb S_1 \rrb(s)))$ \\
+ $S\llb if ~B~ then ~S_1~ else ~S_2~ \rrb = \lambda v . (S \llb S_b \rrb(v))$ \\
+ where $b = B\llb B \rrb (v) + 1$ \\
+ $S\llb I := E \rrb = \lambda v: (v \oplus \{ I \mapsto E \})$
+ }
+ \halfpages{
+ $E ::= E_1 + E_2 \mid I \mid N$
+ }{
+ $E: \state \to \N$ \\
+ $E\llb E_1 + E_2 \rrb = \lambda v . (E\llb E_1 \rrb(v) + E\llb E_2 \rrb(v))$ \\
+ $E\llb I \rrb = \lambda v . v(I)$ \\
+ $E\llb N \rrb = \lambda v . N$
+ }
+ \halfpages{
+ $B ::= E_1 = E_2 \mid \lnot B$
+ }{
+ $B: \state \to \{0,1\}$ \\
+ $B\llb E_1 = E_2 \rrb = \lambda v . (if ~\llb E_1 \rrb(v) = \llb E_2 \rrb(v) ~then~ 1 ~else~ 0)$
+ }
+ \halfpages{
+ $I ::= $ variable identifier
+ }{~}
+ \halfpages{
+ $N ::= \N$
+ }{~}
+ \label{fig:denotational-semantics-example}
+\end{figure}
+
+
A program's semantics can be realised by considering the possible
values for each variable at each point in the program, which we will
@@ -22,9 +81,9 @@ particular point
As a formalisation of these notions we can consider these to be
defined as follows:
\begin{align*}
- \Env: {} & X \to \Z \\
- \PP: {} & \{ \text{program points} \} \\
- \States: {} & \PP \times \Env
+ \Env:& X \to \Z \\
+ \PP:& \{ \text{program points} \} \\
+ \States:& \PP \times \Env
\end{align*}
diff --git a/tex/thesis/references.bib b/tex/thesis/references.bib
index a68e126..d85dea7 100644
--- a/tex/thesis/references.bib
+++ b/tex/thesis/references.bib
@@ -150,3 +150,14 @@
journal = {Transactions of the American Mathematical Society},
volume = {83}
}
+@TECHREPORT{SCOTT70B,
+ AUTHOR = {Scott, Dana S.},
+ TITLE = {Outline of a Mathematical Theory of Computation},
+ TYPE = {Technical Monograph},
+ NUMBER = {PRG--2},
+ INSTITUTION = {Oxford University Computing Laboratory},
+ DEPARTMENT = {Programming Research Group},
+ ADDRESS = {Oxford, England},
+ MONTH = {November},
+ YEAR = {1970}
+}
\ No newline at end of file
diff --git a/tex/thesis/thesis.tex b/tex/thesis/thesis.tex
index 51fa0de..e445c41 100644
--- a/tex/thesis/thesis.tex
+++ b/tex/thesis/thesis.tex
@@ -52,6 +52,7 @@
\newcommand\R{\mathbb{R}}
\newcommand\Z{\mathbb{Z}}
\newcommand\CZ{\overline{\Z}}
+\newcommand\N{\mathbb{Z}}
\newcommand\Eps{\mathbb{E}}
\newcommand\llb\llbracket
\newcommand\rrb\rrbracket
--
cgit v1.2.3