1 files changed, 78 insertions, 47 deletions
diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex
index 983bb44..d223f36 100644
--- a/tex/thesis/litreview/litreview.tex
+++ b/tex/thesis/litreview/litreview.tex
@@ -276,14 +276,11 @@ interpretation over zones.
   \end{figure}
 
   We now attempt to derive a system of inequalities from this for the
-  \emph{least upper bound} of $x$ at each program point.
-  \begin{align*}
-    ub: {} & ~\Vars \to \CZ \\
-    ub(x) &= \min\{v \in \CZ ~|~ x \le v\}.
-  \end{align*}
-  We wish to find a value for $ub(x)$ at each program point in our
-  original program. We denote these values by $ub_A(x)$, $ub_B(x)$ and
-  $ub_C(x)$.
+  \emph{least upper bound} of a variable $x$ at each program
+  point. That is, we want to find a value $ub(x)$ such that, for all
+  possible executions of the program $x \le ub(x)$. We wish to find a
+  value for $ub(x)$ at each program point in our original program. We
+  denote these values by $ub_A(x)$, $ub_B(x)$ and $ub_C(x)$.
 
   For $A$ the value of $x$ is entirely unknown, so no useful bound can
   be given. The possible values of $x$ are bounded only by the top
@@ -370,10 +367,14 @@ equation system can be constructed to aid us in locating the
 
 For every partial-ordering on a set there exists an equivalent
 lattice, defined in terms of a meet operator ($\vee$) and a join
-operator ($\land$), which are defined by the following relationships:
+operator ($\land$), which are defined by:
 \begin{align*}
-  x \le y ~&\iff~ x \vee y = y \\
-  x \le y ~&\iff~ x \land y = x
+  x \vee y = z \iff z \ge x, z \ge y, (w \ge x, w \ge y \implies w \ge
+  z, \forall w) \\
+  x \land y = z \iff z \le x, z \le y, (w \le x, w \le y \implies w \le
+  z, \forall w)
+  %x \le y ~&\iff~ x \vee y = y \\
+  %x \le y ~&\iff~ x \land y = x
 \end{align*}
 
 In the case of Example \ref{example:partial-ordered-construction},
@@ -595,47 +596,77 @@ constraint system.
 
 \section{Min-cost flow}
 
-This matrix fomulation sufficient to calculate bounds on individual
+The matrix formulation is sufficient to calculate bounds on individual
 program variables, as in the interval domain, but in doing so there is
 a significant loss of precision. In order to reclaim some of this
-precision we can use a relational domain. 
-
-
-
-
-
-\endinput
-
-\subsection{Example solve}
-\label{sec-1-3-5}
-
+precision we use a relational domain, such as zones.
 
-Reconsidering our earlier equation system, we now attempt to find
-the minimal fixpoint by means of \emph{policy iteration} and
-\emph{fixpoint iteration}.
+We use a ``template constraint matrix'' to specify interesting values
+for our analysis. A template constraint matrix is an $m \times n$
+matrix, where $n$ is the number of program variables and $m$ is the
+number of interesting abstract values.
 
-\begin{eqnarray*}
-x &=& \max(1, \min(x, 99) + 1) \\
-\end{eqnarray*}
-
-At the beginning and end of each player's turn we will have a variable
-assignment $\{ x \to ? \}$, which will start with the value
-$\{ x \to -\infty \}$.
+\begin{example}
+  If we have two program variables $x_1$ and $x_2$ then we can analyse
+  for values $x_1$, $-x_1$, $x_2$, $-x_2$, $(x_1 - x_2)$ and $(x_2 -
+  x_1)$. If we are only interested in the values of $x_1$, $x_2$ and
+  $(x_2 - x_1)$ then we set our template constraint matrix to be
+  \begin{align*}
+    T &= \left[\begin{array}{cc}
+        1 & 0 \\
+        0 & 1 \\
+        -1 & 1
+      \end{array}\right]
+  \end{align*}
+\end{example}
 
-The $\max$ player then gets a chance to play. They choose to improve
-the strategy by choosing for $x$ to take the value $1$. The $\min$
-player then has no choice but to find a variable assignment $\{ x
-\to 1 \}$, as the $\max$ player has left them no choice.
+This template constraint matrix also specifies the topology of a
+graph. By considering each row as an edge, and each column as a node,
+we can produce a directed graph $G$, such that for each row an edge
+exists between the column containing a $1$ and the column containing a
+$-1$ in that row. In order to guarantee that all rows exist in $G$ it
+is also necessary to add an extra ``dummy node'' such that any
+unspecified edges are adjacent to the dummy node.
 
-Play then returns to the $\max$ player who chooses, again, to improve
-their strategy to instead map $x$ to $\min(x, 99) + 1$. This time the
-$\min$ player must make a decision. It solves $x = \min(x, 99) + 1$
-for it's maximal fixpoint, deciding to use the $99$ value (as the $x$
-value will grow without bound with the $+ 1$, thereby making $99$ the
-minimum of the two options) and returning $\{ x \to 100 \}$ as
-the new assignment.
+\begin{example}
+  For the template constraint matrix
+  \begin{align*}
+    T &= \left[\begin{array}{cc}
+        1 & 0 \\
+        0 & 1 \\
+        -1 & 1
+      \end{array}\right]
+  \end{align*}
 
-The $\max$ player has no further way to improve their strategy, as $1
-< 100$, so the game is over. The minimal fixpoint of the original
-system has been found as $x = 100$.
+  \noindent we construct a directed graph
+
+  \begin{center}
+    \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+        distance=2.5cm]
+      \node (x1)[draw,circle] {$x1$};
+      \node (x2)[draw,circle,below of=x1] {$x2$};
+      \node (dummy)[draw,circle,below right of=x1] {dummy};
+
+      \path
+      (x1) edge[->,bend left] node {} (dummy)
+      (x2) edge[->,bend left] node {} (x1)
+      (x2) edge[->,bend left] node {} (dummy);
+    \end{tikzpicture}.
+  \end{center}
+\end{example}
 
+Once we have determined the topology of this graph, we then perform
+abstract interpretation by assigning the nodes ``supplies'' and the
+edges ``costs''. The supplies correspond to a statement's semantics,
+capturing the combination of variables which are the result of a given
+assignment, while the costs consider the incoming values of variables
+into the statement.
+
+We use the min-cost flow problem on this graph as an operator in our
+equation systems. We fix the topology and the costs in the graph and
+then consider it as a function of its edge costs, which are the
+abstract values entering this node. The validity of this approach is
+considered by Gawlitza et al.~\cite{EasyChair:117}, where it is shown
+that the min-cost flow problem, when considered as a function of its
+edge weights is monotonic and quasi-expansive, thereby making it a
+valid operator in our equation systems.