diff options
| -rw-r--r-- | tex/thesis/contribution/contribution.tex | 360 | ||||
| -rw-r--r-- | tex/thesis/litreview/litreview.tex | 67 | ||||
| -rw-r--r-- | tex/thesis/references.bib | 11 | ||||
| -rw-r--r-- | 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 |