From f823ccc928ae09a63ffef5b6cfe47966e2da1890 Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Mon, 26 Nov 2012 13:59:29 +1100 Subject: A bunch more writing. Write write write. --- tex/thesis/contribution/contribution.tex | 102 ++++++++++++++++--------------- 1 file changed, 53 insertions(+), 49 deletions(-) (limited to 'tex/thesis/contribution') diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex index 48a5e73..fac83c9 100644 --- a/tex/thesis/contribution/contribution.tex +++ b/tex/thesis/contribution/contribution.tex @@ -50,8 +50,8 @@ In this chapter the main theoretical contribution of this thesis is presented: an extension on a $\max$-strategy iteration algorithm for solving fixpoint equations over the integers with monotonic operators\cite{Gawlitza:2007:PFC:1762174.1762203} (see Section -\ref{sec:gawlitza-algorithm}). We devise an algorithm which runs in -linear time in the best case. +\ref{sec:gawlitza-algorithm}). We devise an algorithm which performs +considerably better for practical equation systems. In this chapter we will begin by presenting the Work-list Depth First Search (W-DFS) fixpoint algorithm developed by Seidl et @@ -135,7 +135,7 @@ 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$. We define - $E_\system \subset E$ to be the preimage of system, that is + $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 @@ -170,16 +170,6 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$. \end{align*} \end{definition} -\begin{definition} - A variable or expression $x$ is said to \textbf{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) - \end{align*} - - If $x$ depends on $y$ then $y$ is said to \emph{influence} $x$. -\end{definition} \section{Fixpoint Iteration} \subsection{Kleene Iteration} @@ -191,7 +181,7 @@ reach the least/greatest solution if there is one to be found, but it will often perform many more evaluations than are necessary. This algorithm is presented in Listing \ref{algo:kleene}. -\begin{algorithm}[H] +\begin{algorithm}[tbphH] \begin{algorithmic} \Function {solvefixpoint} {$\system \in \Systems$} \State $k = 0$ @@ -223,7 +213,7 @@ 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{figure}[tbphH] \begin{align*} x &= \min(0, x - 1) \\ y &= \min(0, \infty \oplus x) & @@ -240,15 +230,41 @@ 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. +performance in the next section by taking into account dependencies +between expressions. + +\begin{definition} + An expression $x$ is said to \textbf{depend} on $y$ if and only if + $x(\rho) \ne x(\varrho)$ and + \begin{align*} + \rho(z) &= \varrho(z) & \forall z \in X \backslash \{y\} \\ + \rho(y) &\ne \varrho(y) + \end{align*} + + Intuitively, $x$ depends on $y$ if and only if a change in the value + of $y$ induces a change in the value of $x$. + + If $x$ depends on $y$ then $y$ is said to \emph{influence} $x$. +\end{definition} + \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 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}. +Several algorithms have been presented in literature for finding +solutions to general fixpoint equation systems. In particular has been +the \emph{topdown solver} of Charlier and Van +Hentenryck\cite{TD-fixpoint} and the \emph{worklist} solver of +Kildall\cite{Kildall:1973:UAG:512927.512945} which has been further +extended by others\cite{Jorgensen94findingfixpoints,FP-efficient}. The +W-DFS algorithm of Seidl et al.\cite{DBLP:tr/trier/MI96-11} is an +attempt to combine the best aspects of these general fixpoint +algorithms. + +The W-DFS algorithm takes into account dependencies between variables +as it solves the system. By taking into account 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} \begin{algorithmic} @@ -343,7 +359,7 @@ The W-DFS algorithm provides us with a \emph{local}, \emph{demand-driven} solver for greatest fixpoints of monotonic fixpoint problems. -\begin{figure}[H] +\begin{figure}[tbphH] \begin{tikzpicture} \node[draw] (full) at (0,-2) { \begin{minipage}{0.3\textwidth} @@ -399,14 +415,10 @@ 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 unevaluated. In order to capture this property we will -define the notion of a \emph{local} solver. +other subsystem unevaluated. We call this algorithm \emph{local}, +because it considers only as many variables as are necessary to +compute the requested values. -\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} \section{$\max$-strategy Iteration} @@ -475,7 +487,7 @@ approach is to perform a loop, improving the strategy at each step, until an equilibrium point is reached. The approach is presented in Listing \ref{algo:naive-strategy}. -\begin{algorithm}[H] +\begin{algorithm}[tbphH] \begin{algorithmic} \Assumptions \begin{tabularx}{0.9\textwidth}{rX} @@ -526,7 +538,7 @@ the W-DFS algorithm presented above in Section \ref{sec:wdfs}. Listing \ref{algo:adapted-wdfs} presents one variation on W-DFS to solve $\max$-strategy iteration problems. -\begin{algorithm}[H] +\begin{algorithm}[tbphH] \begin{algorithmic} \Globals \begin{tabularx}{0.9\textwidth}{rX} @@ -665,7 +677,8 @@ stabilises (at which point the fixpoint will also stabilise). 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}). +be \emph{local}, considering only the subset of variables necessary to +calculate the values we are interested in.. @@ -701,7 +714,7 @@ This algorithm is presented in three parts. \subsection{Top level} \label{sec:ldsi:top-level} -\begin{algorithm}[H] +\begin{algorithm}[tbphH] \begin{algorithmic} \Globals \begin{tabularx}{0.9\textwidth}{rX} @@ -749,7 +762,7 @@ in Sections \ref{sec:wdfs} and \ref{sec:adapted-wdfs}. The only exception is $\touchedFP$, which is a newly introduced variable to track variables which are touched by the fixpoint iteration steps. -\begin{algorithm}[H] +\begin{algorithm}[tbphH] \begin{algorithmic} \Function {init} {$s \in \Systems$} \State $D = \underline{-\infty}$ @@ -803,7 +816,7 @@ 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{algorithm}[tbphH] \begin{algorithmic} \Function {evalfixpoint} {$x \in X$, $y \in X$} \State $\solve \fixpoint(y)$ @@ -822,7 +835,7 @@ algorithm, except for the fact that $\solve$ has been renamed to $\solve \fixpoint$. $\eval \fixpoint$ performs the same function as the $\eval$ function in Listing \ref{algo:wdfs}. -\begin{algorithm}[H] +\begin{algorithm}[tbphH] \begin{algorithmic} \Procedure {invalidatefixpoint} {$x \in X$} \Comment{Invalidate a fixpoint variable} @@ -863,7 +876,7 @@ set of changed variables for the $\max$-strategy iteration phase. -\begin{algorithm}[H] +\begin{algorithm}[tbphH] \begin{algorithmic} \Procedure {solvefixpoint} {$x \in X$} \If {$x \not \in \stableFP$} @@ -909,7 +922,7 @@ being stabilised. -\begin{algorithm}[H] +\begin{algorithm}[tbphH] \begin{algorithmic} \Function {evalstrategy} {$x \in E_{\max}$, $y \in E_{\max}$} \State $\solve \strategy(y)$ @@ -957,7 +970,7 @@ directly, but if it is dependent on its own value (as in $\{ x = x + 1 \}$, for example), then it will be destabilised by the transitivity of $\invalidate \strategy$. -\begin{algorithm}[H] +\begin{algorithm}[tbphH] \begin{algorithmic} \Procedure {invalidatestrategy} {$x \in E_{\max}$} \If {$x \in \stableSI$} @@ -982,7 +995,7 @@ by a $\solve \strategy$ call. All $\max$-expressions which (transitively) depend on $x$ are destabilised recursively. -\begin{algorithm}[H] +\begin{algorithm}[tbphH] \begin{algorithmic} \Procedure {solvestrategy} {$x \in E_{\max}$} \If {$x \not \in \stableSI$} @@ -1019,13 +1032,6 @@ Section \ref{sec:adapted-wdfs}. \subsection{Correctness} \label{sec:ldsi:correctness} -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, $\solnFP(s) : X \to D$ for the system $s = \sigma(\system)$. If we consider all valid fixpoints, $\fix(s) = \{ @@ -1187,6 +1193,4 @@ correctly solve their respective portions of the problem, and the communication between them is correct, then we know that the overall algorithm is correct. - \subsection{Implementation} \label{sec:ldsi:implementation} - -- cgit v1.2.3