Thesis and performance testing related stuff.

1 files changed, 49 insertions, 46 deletions

diff --git a/tex/thesis/introduction/introduction.tex b/tex/thesis/introduction/introduction.tex
index d1b1a39..cf32e3d 100644
--- a/tex/thesis/introduction/introduction.tex
+++ b/tex/thesis/introduction/introduction.tex
@@ -10,45 +10,53 @@
 
 In today's increasingly technological world, software bugs can have
 significant consequences, ranging from the relatively minor
-frustration caused to average users to causing deaths. There have been
-several incidents in recent years in which a bug in a software system
-has led directly to injury or death. X-ray machines which provide too
-high a dose of radiation, cars which continue to accelerate against
-the driver's wishes and other dangerous situations have all come about
-as a direct result of software bugs.
+frustration caused to average users, to causing deaths. There have
+been several incidents in recent years in which a bug in a software
+system has led directly to injury or death. X-ray machines which
+provide too high a dose of radiation, cars which continue to
+accelerate against the driver's wishes and other dangerous situations
+have all come about as a direct result of software bugs.
 
 Software bugs also have significant financial costs, with Hailpern and
 Santhanam static that debugging, verification and testing can easily
 comprise 50\% to 75\% of the total development cost of a
-system\cite{Hailpern01softwaredebugging}.
+system~\cite{Hailpern01softwaredebugging}.
 
-In order to limit the number of bugs we have it has become commonplace
-to employ sophisticated approaches to testing. Many different types of
-testing are done to attempt to ensure that software is bug-free. These
-tests, although extremely useful, are inherently incapable of
+In order to limit the number of bugs in a software system, it has become commonplace
+to employ sophisticated testing approaches. Different testing 
+strategies aim to ensure that a software system is bug-free. These
+testing strategies, although extremely useful, are inherently incapable of
 \emph{guaranteeing} that software is free of bugs. This is especially
 a problem in critical software systems, such as those found in
-aeroplanes or large industrial machinery, where software failure can
+aeroplanes or large industrial machinery, where software failures can
 have catastrophic consequences.
 
-In order to provide a guarantee that software is free of bugs we must
-in some way \emph{verify} the software before running it. While it is
-possible to write programs in a way that is easier to verify, it is
-still a difficult and expensive process to provide verification.
-
-There has been a continuous stream of research into automatically
-analysing programs in order to identify bugs from the late 70s to the
-present\cite{CousotCousot77-1,EasyChair:117}. This work is broadly
-classed \emph{static analysis} and this thesis contributes to this
-work.
-
-Due to Rice's Theorem\cite{Rice} we know that there is no general way
-to statically infer properties of programs. In order to overcome this
-many approaches to static analysis have been developed, including the
-framework of abstract interpretation presented by Cousot and
-Cousot\cite{CousotCousot77-1}. In this framework we consider a program
-in a simplified, \emph{abstract}, domain. This allows us to perform a
-sound analysis in general at the expense of precision.
+In order to provide a guarantee that software is free of bugs we
+employ \emph{software verification}, that analyses software without
+running it.  While it is possible to write programs amenable for
+software verification, it is still a difficult and expensive process
+to perform verification on a software system.
+
+There has been a continuous stream of research in
+program analysis for finding bugs starting from the late 70s to the
+present~\cite{CousotCousot77-1,EasyChair:117}. This work is broadly
+categorised as \emph{static program analysis}, and this thesis contributes 
+to this research area.
+
+Due to Rice's Theorem~\cite{Rice} we know that it is undecidable to
+statically infer properties of programs. In order to overcome this
+limitation, many approaches to static analysis have been devised
+including the framework of abstract interpretation introduced by
+Cousot and Cousot~\cite{CousotCousot77-1}. To overcome the
+undecidability issues of static program analysis, a program is
+represented in an abstract domain which becomes decidable. A
+connection (also known as homomorphism) between the abstract domain
+and the concrete domain (actual semantics of the program) is
+established.  This connection is called a Galois-connection and
+provides a proof framework to show that the static program analysis is
+a ``sound'' approximation of the semantics.  The precision of the
+analysis depends on the granularity of the approximation. In general,
+more precise program analyses result in higher complexity classes.
 
 Two abstract domains which are particularly well-known and useful are
 those of \emph{interval} and \emph{zones}. The interval abstract
@@ -62,29 +70,23 @@ analysis, thereby avoiding false-positives, at the cost of speed.
 The process of determining appropriate bounds for program variables
 has traditionally been performed by performing several Kleene
 iterations, followed by a \emph{widening} and \emph{narrowing}. These
-widening and narrowing operators ensure termination, but once again at
-the cost of precision. As an alternative to these operators we can, in
-some instances, use a game-theoretic approach to compute the abstract
-semantics of a program\cite{EasyChair:117}. This approach is less
+widening and narrowing operators ensure termination, but  at
+the cost of precision. As an alternative, we employ in this work  
+a game-theoretic approach to compute the abstract
+semantics of a program~\cite{EasyChair:117}. This approach is less
 general than widening and narrowing, but performs precise abstract
 interpretation over zones.
 
-In this thesis we present an implementation of this game-theoretic
-algorithm, along with our own enhancements which improve its
-performance on real-world data.
-
-
-
 
 \section{Contribution}
 
 In this thesis we present an implementation of the strategy-iteration
 based static analyser presented by Gawlitza et
-al.\cite{EasyChair:117}. Our implementation has several enhancements
+al.~\cite{EasyChair:117}. Our implementation has several enhancements
 which significantly improve the practical performance of the analyser
 on real-world programs.
 
-Theoretical contribution:
+We present one major theoretical contribution:
 \begin{enumerate}
 \item
   We present a demand-driven strategy improvement algorithm for
@@ -92,19 +94,18 @@ Theoretical contribution:
   $\max$ operators.
 \end{enumerate}
 
-Systems contribution:
+We present several systems contributions:
 \begin{enumerate}
 \item
   We develop a solver for monotonic, expansive equation systems based
-  on the work of Gawlitza et al.\cite{EasyChair:117} with several
+  on the work of Gawlitza et al.~\cite{EasyChair:117} with several
   improvements.
 \item
   We analyse the performance of our improved solver on a set of
   equation systems to demonstrate the effect of our improvements.
 \item
   We integrate our solver into the LLVM/Clang
-  framework\cite{LLVM,LLVM-paper,Clang} to perform analysis over
-  Zones\cite{mine:padoII}.
+  framework~\cite{LLVM,LLVM-paper,Clang} to perform analysis over Zones~\cite{mine:padoII}.
 \item
   We analyse the performance of our LLVM analysis on various program
   inputs.
@@ -124,3 +125,5 @@ Our implementation is discussed in Chapter
 \ref{chap:implementation}. We discuss several aspects of our
 implementation before evaluating the results of our analysis on
 several programs.
+
+We draw our conclusion in \ref{chap:conclusion}.