Thesis updating.

1 files changed, 258 insertions, 168 deletions

diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex
index f227112..d2c5d6f 100644
--- a/tex/thesis/litreview/litreview.tex
+++ b/tex/thesis/litreview/litreview.tex
@@ -122,9 +122,9 @@ We can now begin our construction of our collecting semantics
 $V^\#[v], \forall v \in N$.
 
 \begin{align}
-V^\# [st] &\ge \alpha(\Z^n) \label{eqn:start-node} \\
-V^\# [v] &\ge \llb s_{(u,v)} \rrb ^\# (V^\# [u]) & \forall (u,v) \in
-E \label{eqn:confluence}
+  V^\# [st] &\ge \alpha(\Z^n) \label{eqn:start-node} \\
+  V^\# [v] &\ge \llb s_{(u,v)} \rrb ^\# (V^\# [u]) & \forall (u,v) \in
+  E \label{eqn:confluence}
 \end{align}
 
 In the first equation, the possible abstract states of the start node
@@ -187,29 +187,34 @@ concretization functions.
   \label{example:partial-ordered-construction}
 
   As an example, let us consider the following program:
-
-  \begin{lstlisting}
+  
+  \begin{figure}[here]
+    \begin{minipage}{5cm}
+      \begin{lstlisting}
     x = 1
     while x <= 99:
-    x = x + 1
-  \end{lstlisting}
-
-  \begin{figure}
-    \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
-        distance=2cm,main node/.style={circle,fill=blue!20,draw},every
-        loop/.style={min distance=1.5cm}]
-      
-      \node[main node] (A) {$A$};
-      \node[main node] (B) [below of=A] {$B$};
-      \node[main node] (C) [below of=B] {$C$};
-      
-      \path[every node/.style={fill=none}]
-      (A) edge node[right]{$x = 1$} (B)
-      (B) edge [loop right] node[right]{$x \le 99: x = x + 1$} (B)
-      (B) edge node[right]{$x > 99$} (C);
-      
-    \end{tikzpicture}
-    \caption{The CFG for Example
+      x = x + 1
+      \end{lstlisting}
+    \end{minipage}
+    \hfill
+    \begin{minipage}{0.45\textwidth}
+      \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+          distance=2cm,main node/.style={circle,fill=blue!20,draw},every
+          loop/.style={min distance=1.5cm}]
+        
+        \node[main node] (A) {$A$};
+        \node[main node] (B) [below of=A] {$B$};
+        \node[main node] (C) [below of=B] {$C$};
+        
+        \path[every node/.style={fill=none}]
+        (A) edge node[right]{$x = 1$} (B)
+        (B) edge [loop right] node[right]{$x \le 99: x = x + 1$} (B)
+        (B) edge node[right]{$x > 99$} (C);
+        
+      \end{tikzpicture}
+    \end{minipage}
+    
+    \caption{Program and CFG for Example
       \ref{example:partial-ordered-construction}}
     \label{fig:partial-ordered-construction}
   \end{figure}
@@ -218,9 +223,10 @@ concretization functions.
   \ref{fig:partial-ordered-construction}.
 
   We will now attempt to derive a system of inequalities from this for
-  the \emph{upper bound} of $x$:
+  the \emph{least upper bound} of $x$:
   \begin{align*}
-    ub(x) &= v \in \CZ \text{ such that } x \le v & \forall x \in \Z
+    ub: & ~\text{\bf Vars} \to \CZ \\
+    ub(x) &= \min\{v \in \CZ ~|~ x \le v\}
   \end{align*}
 
   For $A$ the value of $x$ is entirely unknown, so no useful bound can
@@ -275,7 +281,8 @@ concretization functions.
 \end{example}
 
 
-\subsubsection{Lattice construction}
+\subsection{Lattice construction}
+\label{subsec:lattice-construction}
 
 The partial-ordering formulation considered above is a helpful
 presentation of the problem in terms of constraints, but an equivalent
@@ -291,164 +298,247 @@ operator ($\land$), which are defined by the following relationships:
 \end{align*}
 
 In the case that we are considering, with $x, y \in \CZ$, the meet and
-join operators correspond with $\min$ and $\max$, respectively. This
-allows us to simplify our original system of inequalities to the
-following:
+join operators correspond with $\max$ and $\min$, respectively. This
+allows us to simplify the system of inequalities in Example
+\ref{example:partial-ordered-construction} to the following following:
 \begin{align*}
-  ub(x_A) &\ge \infty \\
-  ub(x_B) &\ge \max(1, \min(ub(x_B), 99) + 1) \\
-  ub(x_C) &\ge ub(x_B)
+  ub(x_A) &= \infty \\
+  ub(x_B) &= \max(1, \min(ub(x_B), 99) + 1) \\
+  ub(x_C) &= ub(x_B)
 \end{align*}
 
 The two constraints on the upper bound of $x_B$ can be combined into
-the one constraint by taking the maximum of the two constraints (that
-is, by meeting the less restrictive constraint). This ensures that if
-the combined constraint is satisfied then both of the original
-constraints must also be satisfied.
-
-
-
-%\begin{example}
-
-In order to determine a lower bound for $x$ at each program point it
-is sufficient to determine an \emph{upper} bound for $-x$. For our
-second example we will consider the following program fragment:
-
-\begin{lstlisting}
-x = 0
-y = x
-while x < 10:
-  x = x + 1
-  y = y + x
-\end{lstlisting}
-
-This program, as a CFG:
-
-\begin{center}
-\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
-    distance=2cm,main node/.style={circle,fill=blue!20,draw},every
-    loop/.style={min distance=1.5cm}]
-
-  \node[main node] (A) {$A$};
-  \node[main node] (B) [below of=A] {$B$};
-  \node[main node] (C) [below of=B] {$C$};
-  
-  \path[every node/.style={fill=none}]
-  (A) edge node[right]{$x = 0; y = x$} (B)
-  (B) edge [loop right] node[right]{$x < 10: x = x + 1; y = y + x$} (B)
-  (B) edge node[right]{$x \ge 10$} (C);
-  
-\end{tikzpicture}
-\end{center}
-
-%\end{example}
+one constraint by taking the maximum of them. This is because $x >
+\max(a, b) ~\implies~ x > a \text{ and } x > b$
 
-We will now try to derive an equation system for the \emph{upper} and
-\emph{lower} bounds of $x$ and $y$.
 
-In order to properly capture the state of the variables at each state
-we will consider the abstract state as a vector of the form $(x_u,
--x_l, y_u, -y_l)$. $x_u$ and $y_u$ are the upper bounds of $x$ and $y$
-respectively. $x_l$ and $y_l$ are the lower bounds of $x$ and $y$,
-which are then negated, as explained above, to convert them into upper
-bound problems.
 
-Each statement in our example program is now a transformation on a
-vector rather than a scalar (as our original example was). This makes
-the equation system significantly more complex.
-
-Let us begin by deriving the equation system for the simplest node in
-the CFG, $A$.
-
-\begin{eqnarray*}
-  \left(\begin{array}{c}
-    x_u \\ y_u \\ -x_l \\ -y_l
-  \end{array}\right)_A
-  &=&
-  \left(\begin{array}{c}
-    \infty \\ \infty \\ \infty \\ \infty
-  \end{array}\right)
-\end{eqnarray*}
-
-This is the same as saying that $x$ and $y$ each lie within the range
-$[-\infty, \infty]$. In other words: both $x$ and $y$ are unbounded at
-node $A$ and we know nothing of their possible values.
-
-For node $B$ we, again, must take into account two transformations to
-our state. The first is by the edge $A \to B$, the second by
-the edge $B \to B$. We then take the less-restrictive of these
-two bounds (which, again, is the $\max$ of the two).
-
-Let us begin with $A \to B$.
+\begin{example}
+  \label{example:both-bounds}
+
+  In order to determine a lower bound for $x$ at each program point it
+  is sufficient to determine an \emph{upper} bound for $-x$. For our
+  second example we will consider the following program fragment:
+
+  \begin{figure}[here]
+    \begin{minipage}{5cm}
+      \begin{lstlisting}
+    x = 0
+    while x <= 9:
+      x = x + 1
+      \end{lstlisting}
+    \end{minipage}
+    \hfill
+    \begin{minipage}{0.5\textwidth}
+      \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+          distance=2cm,main node/.style={circle,fill=blue!20,draw},every
+          loop/.style={min distance=1.5cm}]
+        
+        \node[main node] (A) {$A$};
+        \node[main node] (B) [below of=A] {$B$};
+        \node[main node] (C) [below of=B] {$C$};
+        
+        \path[every node/.style={fill=none}]
+        (A) edge node[right]{$x = 0$} (B)
+        (B) edge [loop right] node[right]{$x <= 9: x = x + 1$} (B)
+        (B) edge node[right]{$x > 9$} (C);
+
+      \end{tikzpicture}
+    \end{minipage}
+    \caption{Program and CFG for Example \ref{example:both-bounds}}
+    \label{fig:both-bounds}
+  \end{figure}
 
-\begin{eqnarray*}
-\left(\begin{array}{c}
-x_u \\ y_u \\ -x_l \\ -y_l
-\end{array}\right)_{AB}
-&=&
-\left(\begin{array}{c}
-0 \\ 0 \\ 0 \\ 0
-\end{array}\right) \\
-\end{eqnarray*}
+  We will now try to derive an equation system for the \emph{upper}
+  and \emph{lower} bounds of $x$.
+
+  In order to capture the state of the variables at each program point
+  we will consider the abstract state as the two-dimensional vector
+  $(ub(x), -lb(x))$, that is the upper bound of $x$, $ub(x)$, and the
+  \emph{negated} lower bound of $x$, $-lb(x)$. The greatest fixpoint
+  of our system of equations over $\CZ^2$ will then give us our bounds
+  for $ub(x)$ and $lb(x)$.
+
+  To begin with, let us once again consider the node $A$. At the point
+  of $A$ there is no information as to the bounds of $x$, so our
+  constraint must contain the entirety of $\CZ$. This corresponds to
+  $ub(x) = \infty, lb(x) = -\infty$, which gives us the following
+  inequality:
+  \begin{align*}
+    \left(\begin{array}{c}
+      ub(x)_A \\ -lb(x)_A
+    \end{array}\right)
+    &\ge
+    \left(\begin{array}{c}
+      \infty \\ \infty
+    \end{array}\right)
+  \end{align*}
 
-This edge merely sets $x$ to $0$ and $y$ to $x$ (which is now the
-constant $0$), so both the upper and lower bounds are $0$. This is the
-simplest sort of edge possible, as it just sets both bounds to a
-constant.
+  As before, the node $B$ is the first of particular interest to
+  us. With two incoming edges we must have two constraints for this
+  node.
 
-Now, on to $B \to B$.
+  The first constraint comes from the edge $A \to B$. This edge does
+  not do much of interest, it ignores the preceding value of $x$ and
+  simply sets $x$ to $1$. This is captured in the following inequality:
+  \begin{align*}
+    \left(\begin{array}{c}
+      ub(x)_B \\ -lb(x)_B
+    \end{array}\right)
+    &\ge
+    \left(\begin{array}{c}
+      1 \\ -1
+    \end{array}\right)
+  \end{align*}
 
-\begin{eqnarray*}
-  \left(\begin{array}{c}
-    x_u \\ y_u \\ -x_l \\ -y_l
-  \end{array}\right)_{BB}
-  &=&
-  \left(\begin{array}{cccc}
-    1 & 0 & 0 & 0 \\
-    1 & 1 & 0 & 0 \\
-    0 & 0 & 1 & 0 \\
-    0 & 0 & 1 & 1
-  \end{array}\right)
-  \left(\begin{array}{c}
-    \min(x_u, 9) \\ y_u \\ -x_l \\ -y_l
-  \end{array}\right)_B
-  +
-  \left(\begin{array}{c}
-    1 \\ 0 \\ -1 \\ 0
-  \end{array}\right)
-\end{eqnarray*}
+  The constraint from the edge $B \to B$ is somewhat more
+  complicated. The transformation $x = x + 1$ is represented by the
+  matrix/vector operations of multiplication and
+  addition. Multiplication by the identity matrix indicates that $x$
+  itself is present in the right-hand side of the transformation,
+  while the addition of the vector \(\left(\begin{array}{c} 1 \\ -1
+  \end{array}\right) \) captures the effect of the addition on
+  each of the bounds (increasing each of the bounds by one).
+
+  The $x <= 9$ conditional, which is present on the edge, is captured
+  by the restriction on the growth of the upper bound. \(\min(ub(x)_B,
+  9)\) ensures the upper-bound's growth is limited by the value
+  $9$. It should be noted that there is no bound placed on the
+  lower-bound as the program only bounds $x$'s growth from above on
+  this edge.
+  \begin{align*}
+    \left(\begin{array}{c}
+      ub(x)_B \\ -lb(x)_B
+    \end{array}\right)
+    &\ge
+    \left[\begin{array}{cc}
+      1 & 0 \\
+      0 & 1
+    \end{array}\right]
+    \left(\begin{array}{c}
+      \min(ub(x)_B, 99) \\
+      -lb(x)_B
+    \end{array}\right)
+    +
+    \left(\begin{array}{c}
+      1 \\
+      -1
+    \end{array}\right)
+  \end{align*}
 
+  The edge $B \to C$ is quite simple as it simply provides another
+  restriction on the value of $x$ without any further
+  transformation. This restriction is placed on the lower-bound of $x$
+  only (leaving the upper-bound unchanged) and is captured by the
+  following inequality:
+  \begin{align*}
+    \left(\begin{array}{c}
+      ub(x)_C \\
+      -lb(x)_C
+    \end{array}\right)
+    &\ge
+    \left(\begin{array}{c}
+      ub(x)_B \\
+      \min(-lb(x)_B, 99)
+    \end{array}\right)    
+  \end{align*}
 
+  This gives us the following inequalities for this program:
+  \begin{align*}
+    \left(\begin{array}{c}
+      ub(x)_A \\ -lb(x)_A
+    \end{array}\right)
+    &\ge
+    \left(\begin{array}{c}
+      \infty \\ \infty
+    \end{array}\right)
+    \\
+    \left(\begin{array}{c}
+      ub(x)_B \\ -lb(x)_B
+    \end{array}\right)
+    &\ge
+    \left(\begin{array}{c}
+      1 \\ -1
+    \end{array}\right)
+    \\
+    \left(\begin{array}{c}
+      ub(x)_B \\ -lb(x)_B
+    \end{array}\right)
+    &\ge
+    \left[\begin{array}{cc}
+      1 & 0 \\
+      0 & 1
+    \end{array}\right]
+    \left(\begin{array}{c}
+      \min(ub(x)_B, 99) \\
+      -lb(x)_B
+    \end{array}\right)
+    +
+    \left(\begin{array}{c}
+      1 \\
+      -1
+    \end{array}\right)
+    \\
+    \left(\begin{array}{c}
+      ub(x)_C \\
+      -lb(x)_C
+    \end{array}\right)
+    &\ge
+    \left(\begin{array}{c}
+      ub(x)_B \\
+      \min(-lb(x)_B, 99)
+    \end{array}\right)
+  \end{align*}
 
+  By combining these expressions as discussed in Section
+  \ref{subsec:lattice-construction} we can obtain the following system
+  of equations:
+  \begin{align*}
+    \left(\begin{array}{c}
+      ub(x)_A \\ -lb(x)_A
+    \end{array}\right)
+    &=
+    \left(\begin{array}{c}
+      \infty \\ \infty
+    \end{array}\right)
+    \\
+    \left(\begin{array}{c}
+      ub(x)_B \\ -lb(x)_B
+    \end{array}\right)
+    &=
+    \max\left(
+    \left(\begin{array}{c}
+      1 \\ -1
+    \end{array}\right),
+    \left[\begin{array}{cc}
+      1 & 0 \\
+      0 & 1
+    \end{array}\right]
+    \left(\begin{array}{c}
+      \min(ub(x)_B, 99) \\
+      -lb(x)_B
+    \end{array}\right)
+    +
+    \left(\begin{array}{c}
+      1 \\
+      -1
+    \end{array}\right)
+    \right)
+    \\
+    \left(\begin{array}{c}
+      ub(x)_C \\
+      -lb(x)_C
+    \end{array}\right)
+    &=
+    \left(\begin{array}{c}
+      ub(x)_B \\
+      \min(-lb(x)_B, 99)
+    \end{array}\right)
+  \end{align*}
 
-\begin{eqnarray*}
-  \left(\begin{array}{c}
-    x_u \\ y_u \\ -x_l \\ -y_l
-  \end{array}\right)_B
-  &=&
-  \max\left(
-  \left(\begin{array}{c}
-    x_u \\ y_u \\ -x_l \\ -y_l
-  \end{array}\right)_{AB},
-  \left(\begin{array}{c}
-    x_u \\ y_u \\ -x_l \\ -y_l
-  \end{array}\right)_{BB}
-  \right)
-\end{eqnarray*}
+\end{example}
 
-The bounds for $x$ and $y$ at node $C$ are very similar to those at
-node $B$, except that $x$ has one additional constraint added to it on
-the bottom. This changes its equation system slightly.
 
-\begin{eqnarray*}
-  \left(\begin{array}{c}
-    x_u \\ y_u \\ -x_l \\ -y_l
-  \end{array}\right)_C
-  &=&
-  \left(\begin{array}{c}
-    x_u \\ y_u \\ -x_l \\ -y_l
-  \end{array}\right)_{B}
-\end{eqnarray*}
 
 
 \subsection{Formalities}