thesis.tex

\documentclass[12pt,twoside,openright]{book}

\usepackage{setspace}
\doublespacing
\usepackage[left=1.5in,right=1in,top=1in,bottom=1in]{geometry}

% display date and time of when PDF was made
%\input{now}
\usepackage{fancyhdr}
\pagestyle{fancy}
\fancyhead{}
\fancyhead[LE]{\leftmark}
\fancyhead[RO]{\rightmark}
\fancyfoot{}
\fancyfoot[LE,RO]{\thepage}
%\fancyfoot[RE,LO]{\scriptsize\rightnow}
\renewcommand{\headrulewidth}{0pt}
\headheight 14.5pt


\usepackage{url}
\usepackage{longtable}
\usepackage{multirow}
\usepackage{comment}
\usepackage{marvosym}

\input{polycode.lhs.tex}

%\def\TODO#1{\par\noindent{}TODO:~\ldots\emph{#1}\ldots\par}
\def\TODO#1{\noindent{}TODO:~\ldots\emph{#1}\ldots}

\def\source#1{}

\usepackage{amsmath}
\usepackage{amsthm}
\newtheorem{theorem}{Theorem}[chapter]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}

\def\eqName#1{\textsf{\mdseries(#1)}}
\def\eqTag#1{\tag*{\eqName{#1}}}


\usepackage{mathpartir}
\def\TirName#1{\eqName{#1}}

\usepackage[pdftex,matrix,arrow,curve,color]{xy}
% for arrow labels in xymatrix
\usepackage{rotating}
\def\xyrot#1#2{\begin{turn}{#1}\parbox[c][1.5ex][c]{1.5ex}{\makebox[1.5ex][c]{$#2$}}\end{turn}}
% agda-mode doesn't like {-
\def\xyar{\ar@{->}}
\def\xyarr{\ar@{->>}}

% vector lookup for verified chapter
\def\index[#1]{\!\texttt[#1\texttt]\!}

% lhs2TeX
%{{{%
\usepackage[pdftex]{color}

\renewcommand\hsindent[1]{\quad}
\setlength{\mathindent}{2ex}
\DeclareMathAlphabet{\mathkw}{OT1}{cmss}{bx}{n}

\newcommand\keyw[1]{\textcolor[rgb]{.75,.4,0}{\mathkw{#1}}}
\newcommand\type[1]{\textcolor[rgb]{0,0,.75}{\mathsf{#1}}}
\newxyColor{type}{0 0 0.75}{rgb}{}
% \newcommand\tcls[1]{\textcolor[rgb]{.25,0,.75}{\mathsf{#1}}}
\newcommand\cons[1]{\textcolor[rgb]{0,.5,0}{\mathsf{#1}}}
\newcommand\dstr[1]{\textcolor[rgb]{.75,.75,0}{\mathsf{#1}}}
\newcommand\func[1]{\textcolor[rgb]{.75,0,0}{\mathsf{#1}}}
\newcommand\ltrl[1]{\textcolor[rgb]{.6,0,.6}{\mathtt{#1}}}
\newcommand\name[1]{\textcolor[rgb]{.75,0,.75}{\mathsf{#1}}}
\newcommand\commentstyle[1]{\textcolor[rgb]{0,.6,0.75}{#1}}
\newcommand\shed[1]{\colorbox[rgb]{.6,1,.6}{#1}}

\def\hide#1{}

\newcommand\Prime{\ensuremath{'}}
\newcommand\PPrime{\ensuremath{''}}
\newcommand\PPPrime{\ensuremath{'''}}

\newcommand\prefix[1]{#1\,}
\newcommand\postfix[1]{\,#1}

\newcommand\infix[1]{\mathbin{#1}}
\newcommand\infixL[1]{\infix{#1}\!}
\newcommand\infixM[1]{\!\infix{#1}\!}
\newcommand\infixR[1]{\!\infix{#1}}
%}}}%



% \includeonly{semantics,agda.lagda}
\begin{document}

\pagestyle{empty}
\begin{titlepage}
\begin{center}
\vspace*{1in}
{\LARGE Compiling Concurrency Correctly}
\par
{\Large Verifying Software Transactional Memory}
\par
\vspace{1.5in}
{\large Liyang HU}
\par
\vfill
A Thesis submitted for the degree of Doctor of Philosophy
\par
\vspace{0.5in}
School of Computer Science
\par
\vspace{0.5in}
University of Nottingham
\par
\vspace{0.5in}
June 2012
\end{center}
\cleardoublepage
\end{titlepage}


\pagestyle{fancy}
\pagenumbering{roman}

%{{{%
\begin{center}
{\large\bf Abstract}
\end{center}

Concurrent programming is notoriously difficult, but with multi-core
processors becoming the norm, is now a reality that every programmer must
face. Concurrency has traditionally been managed using low-level mutual
exclusion \emph{locks}, which are error-prone and do not naturally support
the compositional style of programming that is becoming indispensable for
today's large-scale software projects.

A novel, high-level approach that has emerged in recent years is that of
\emph{software transactional memory} (STM), which avoids the need for
explicit locking, instead presenting the programmer with a declarative
approach to concurrency. However, its implementation is much more complex
and subtle, and ensuring its correctness places significant demands on the
compiler writer.

This thesis considers the problem of formally verifying an implementation of
STM. Utilising a minimal language incorporating only the features that we
are interested in studying, we first explore various STM design choices,
along with the issue of compiler correctness via the use of automated
testing tools. Then we outline a new approach to concurrent compiler
correctness using the notion of bisimulation, implemented using the Agda
theorem prover. Finally, we show how bisimulation can be used to establish
the correctness of a low-level implementation of software transactional
memory.

%}}}%

\chapter*{Acknowledgements}

Many have had a part to play in this production, and I cannot hope to
enumerate them exhaustively. Nevertheless, I would like to begin by thanking
everyone at the Functional Programming Laboratory in Nottingham who have
made it such an interesting place, academically and socially. Conor McBride
deserves a special mention for his multitudes of infectious ideas that
started me on this dependently-typed journey, as do Ulf Norell and Nils
Anders Danielsson for the years they have put into Agda and its standard
library that underpins a large part of this work.

There were plenty of ups and downs in the process. I am eternally grateful
to my flatmate Rebecca who had a large part in maintaining my sanity, my
muse Ana whose company kept my spirits up through those seemingly endless
hours of writing, and my friend Tom for sharing his inexhaustible enthusiasm
with me. The numerous thoughtful gifts from Star and Cosmo are also warmly
received. I am very fortunate to have my parents, whose support made my
aspirations possible. Thank you all.

I appreciate the effort of Andy Gordon and Thorsten Altenkirch in
undertaking the rewardless task of my examination. Tsuru Capital---as well
as being an excellent place to work---afforded me much time and flexibility
with which to complete my corrections. Last but certainly not least, I would
like to express my gratitude towards my supervisor Graham Hutton for his
guidance and enduring patience through all these years, without whose
insights and encouragement this thesis would certainly have found itself in
perpetual limbo.

\tableofcontents
%\listoffigures

{\include{introduction.lhs}}
{\include{stm.lhs}}
{\include{semantics}}
{\include{testing.lhs}}
{\include{model.lhs}}
{\include{agda.lagda}}
{\include{nondet.lagda}}
{\include{fork.lagda}}
%{\include{verified.lagda}}
{\include{atomic.lagda}}
{\include{conclusion}}

\bibliographystyle{alpha}
\bibliography{thesis}

\end{document}