1 files changed, 491 insertions, 0 deletions
diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex
new file mode 100644
index 0000000..f227112
--- /dev/null
+++ b/tex/thesis/litreview/litreview.tex
@@ -0,0 +1,491 @@
+\chapter{Literature Review} \label{chap:litreview}
+
+\section{Program Semantics}
+
+Let $X$ be the set of program variables, $D$ be the union of all
+possible domains from which variables can come, and $PP$ be the set of
+all edges in the Control Flow Graph of the program.
+
+\begin{eqnarray}
+Env: & X \to D \\
+Expr: & Env \to D \\
+States: & PP \times Env
+\end{eqnarray}
+
+$States$, then, contains every possible state for the program ($Env$)
+at each program point. A more interesting set for us is the set of
+reachable states, this is: states which the program can actually reach
+during execution. This concept of ``reachable states'' allows us to
+formally capture all possible execution states for a program. We can
+further define $Reach(p) = {e \in Env | \le p,e \ge \in States}$
+
+Unfortunately it is unfeasible to analyse the complete semantics of a
+program, due to the sheer number of possible reachable states which
+must be examined. In many cases there are an infinite number of states
+which would have to be considered to ensure a sound analysis of the
+program.
+
+
+\section{Abstract Interpretation} \label{sec:abstract-interpretation}
+\subsection{General Framework}
+
+Cousot and Cousot developed a framework for performing sound program
+analysis called ``Abstract Interpretation''. In this framework we
+consider a program under a set of ``abstract semantics'' which, in
+some sense, simplify the program (and the analysis thereof).
+
+As a simple example one may consider the case of mathematical
+expressions over the integers. The operators \(+,\times\) perform
+operations on these integers, with their semantics being defined as
+one would expect. We may then define an abstract semantic of these
+expressions when considering only signs (and zero), for example. Then
+our abstract states contains four states: ${(+), (-), (\pm), 0}$.
+
+\begin{align*}
+  ( + ) + ( + ) &= ( + ) \\
+  ( + ) + ( - ) &= ( \pm ) \\
+  ( - ) + ( - ) &= ( - ) \\
+    x   + 0 &=   x \\
+  ( \pm ) + x &= ( \pm ) \\
+  ( + ) \times ( + ) &= ( + ) \\
+  ( + ) \times ( - ) &= ( - ) \\
+  ( - ) \times ( + ) &= ( - ) \\
+  0 \times x &=  0 \\
+  ( \pm ) \times x &= ( \pm ), \forall x \ne 0 \\
+\end{align*}
+
+This abstract semantic will give us sound results (any analysis of the
+abstract semantic will correspond to an equivalent analysis of the
+concrete semantic), but will not give us every opportunity for
+analysis (the abstraction may ignore relevant details).
+
+In order to ensure we have a useful abstract interpretation it's
+necessary to provide two operations to map between concrete states and
+abstract states. These operations we call ``abstraction'' (mapping
+from a concrete state to an abstract state), denoted by \(\alpha\),
+and ``concretization'' (mapping from an abstract state to a concrete
+state), denoted by \(\gamma\).
+
+\textbf{Write more about the abstraction/concretization functions}
+
+\subsection{Intervals}
+
+Something about intervals.
+
+\subsection{Zones} \label{subsec:zones}
+
+In order to perform any abstract interpretation we must first
+determine which abstract domain we will consider. Cousot and Cousot
+introduced the abstract domain of ``ranges'' in their original paper
+\cite{CousotCousot77-1}. This domain constrains variables to lie
+within a range \(x \in [a, b]\) with \(x, a, b \in \Z\).
+
+Further work has been done the abstract domain of zones and octagons,
+which are generalised by the template polyhedral abstract domain.
+
+Zones provide an abstract domain in which we try to put a bound on
+either a variable's magnitude ($\pm x \le c$) or to put a bound on the
+difference between two variables ($x - y \le c$).
+
+Octagons generalise this by allowing us to vary the sign on both
+variables to derive a bound as $\pm x \pm y \le c$.
+
+The polyhedral abstract domain is a clear generalisation of both the
+zone and octagon abstract domains in that it determines a bound for an
+arbitrary linear combination of arbitrary program variables. For
+example, finding a bound as $c_0 x_0 + c_1 x_1 + ... + c_n x_n \le c$,
+where $c, c_i \in \R$ and $x_i$ are program variables.
+
+
+\section{Min/max problem}
+
+In \newcite{Gawlitza:2007:PFC:1762174.1762203} a conversion from a
+program's Control Flow Graph (henceforth CFG) to a system of equations
+involving only monotonic, expansive operators is presented. This
+conversion results in an equation system which can be solved in order
+to perform Abstract Interpretation (Section
+\ref{sec:abstract-interpretation}) over Zones (Section
+\ref{subsec:zones}).
+
+\subsection{Partial-ordering Formulation}
+
+To begin our construction of the equation systems we first need to
+formalise one of a CFG. For our purposes we will consider a CFG to be
+a tuple $G = (N, E, S, st)$. A finite set of \emph{control-points}
+$N$, a finite set $E \subseteq N \times N$ of \emph{edges} between
+these control points (ie. if $(u,v) \in E$ then an edge exists in the
+CFG from $u$ to $v$). A mapping $S: N \times N \to Stmt$
+taking each edge in the CFG to a \emph{statement}. $st \in N$ denotes
+the special \emph{start control-point}.
+
+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}
+\end{align}
+
+In the first equation, the possible abstract states of the start node
+must always be the completely unconstrained abstract domain. Any value
+is possible for any variable on the first node of the CFG.
+
+The second equation requires that the possible abstract states of a
+node, $v$, contains either the same amount of information or less
+information than each of the predecessors of $v$ in the CFG.
+
+\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] (V) {$v$};
+    \node[main node] (U) [above left of=V] {$u$};
+    \node[main node] (W) [above right of=V] {$w$};
+    
+    \path[every node/.style={fill=none}]
+    (U) edge node[left]{$s_{(u,v)}$} (V)
+    (W) edge node[right]{$s_{(w,v)}$} (V);
+    
+  \end{tikzpicture}
+  \caption{A simple CFG fragment.}
+  \label{cfg:confluence}
+\end{figure}
+
+So, if we have the CFG fragment shown in Figure \ref{cfg:confluence}
+then we know that $V^\#[v]$ must `contain', or be larger than, each of
+the edges coming in to $v$. In this case there are two incoming edges
+to $v$: $(u,v)$ and $(w,v)$. 
+
+The edge $(u,v)$ leads to the state $\llb s_{(u,v)} \rrb^\#
+(V^\#[u])$y. It is clear that $V^\#[v]$ must be either the same size
+or `larger' than this value, as it must either equal this constraint
+or it must be a looser constraint. This gives us the inequality
+\eqref{eqn:confluence}: $V^\#[v] \ge \llb s_{(u,v)}^\# \rrb
+(V^\#[u])$.
+
+Similarly by considering the edge $(w,v)$ and following the same argument
+we find that $V^\# [v] \ge \llb s_{(w,v)} \rrb ^\# (V^\# [w])$.
+
+For the start node in the CFG this inequality is obviously
+useless. The start node has no predecessors (by definition) and thus
+must have a value that is not dependent on other nodes. We can,
+therefore, simply define the start node's possible abstract states to
+be at least as big as the complete set of abstract states (as in
+\eqref{eqn:start-node}).
+
+We have not yet considered the effect that $s_{(u,v)}, \forall (u,v)
+\in E$ has on the state in each edge. The effect of the statement in
+the abstract domain depends on the statement's effect in the concrete
+domain, but for all statements we define $\llb s \rrb^\# := \alpha
+\circ \llb s \rrb \circ \gamma$. In essence this is just `lifting' the
+statement's effects in the abstract domain with our abstraction and
+concretization functions.
+
+\begin{example}
+  \label{example:partial-ordered-construction}
+
+  As an example, let us consider the following program:
+
+  \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
+      \ref{example:partial-ordered-construction}}
+    \label{fig:partial-ordered-construction}
+  \end{figure}
+
+  This corresponds to the CFG presented in Figure
+  \ref{fig:partial-ordered-construction}.
+
+  We will now attempt to derive a system of inequalities from this for
+  the \emph{upper bound} of $x$:
+  \begin{align*}
+    ub(x) &= v \in \CZ \text{ such that } x \le v & \forall x \in \Z
+  \end{align*}
+
+  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
+  value in $\CZ$, which is $\infty$. This gives us the following
+  inequality for node $A$:
+  \begin{align*}
+    ub(x_A) &\ge \infty
+  \end{align*}
+
+  When we reach $B$ we have two incoming edges. One comes from $B$
+  itself, the other from $A$.
+
+  The edge from $A$ to $B$ is very simple. It has no constraint and
+  simply sets the value of $x$ to $1$. It corresponds to an equation
+  of the form $ub(x_B) \ge 1$.
+
+  The edge from $B$ to itself is somewhat more complex. To begin with
+  it changes the value of $x$ depending on the previous value of
+  $x$. It also is executed conditionally (when $x \le 99$), which will
+  affect the bound on $x$. Because the condition limits the growth of
+  $x$ the corresponding equation for this edge is $ub(x_B) \ge
+  \min(x, 99) + 1$.
+
+  This leaves us with two simultaneous constraints on the value of
+  $ub(x_B)$.
+  \begin{align*}
+    ub(x_B) &\ge 1 \\
+    ub(x_B) &\ge \min(ub(x_B), 99) + 1
+  \end{align*}
+
+  The upper bound on the value of $x$ for node $C$ is the same as the
+  upper bound on the value of $x$ in $B$, because the edge from $B$ to
+  $C$ does not change the value of $x$, nor does it provide any more
+  details about the upper bound of $x$. (It does change the lower
+  bound of $x$, but we have not considered the lower bound in this
+  analysis.)  This gives us a very simple equation system for $C$.
+  \begin{align*}
+    ub(x_C) &\ge ub(x_B)
+  \end{align*}
+
+  So, the upper bounds for $x$ can be found at every program point in
+  our original program by finding the smallest values of $x_A, x_B,
+  x_C$ subject to these constraints:
+  \begin{align*}
+    ub(x_A) &\ge \infty \\
+    ub(x_B) &\ge 1 \\
+    ub(x_B) &\ge \min(ub(x_B), 99) + 1 \\
+    ub(x_C) &\ge ub(x_B)
+  \end{align*}
+
+\end{example}
+
+
+\subsubsection{Lattice construction}
+
+The partial-ordering formulation considered above is a helpful
+presentation of the problem in terms of constraints, but an equivalent
+system can be constructed to aid us in locating the \emph{least}
+solution to the system.
+
+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:
+\begin{align*}
+  x \le y ~&\iff~ x \vee y = y \\
+  x \le y ~&\iff~ x \land y = x
+\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:
+\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)
+\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}
+
+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{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*}
+
+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.
+
+Now, on to $B \to B$.
+
+\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*}
+
+
+
+
+\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*}
+
+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}
+
+
+
+
+\subsection{Example solve}
+\label{sec-1-3-5}
+
+
+Reconsidering our earlier equation system, we will now attempt to find
+the minimal fixpoint by means of \emph{policy iteration} and
+\emph{fixpoint iteration}.
+
+\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 \}$.
+
+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.
+
+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.
+
+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$.
+