\documentclass[11pt,a4paper]{article}
\usepackage[a4paper,margin=1cm,footskip=.5cm]{geometry}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}

\usepackage[english]{babel}

\usepackage{graphicx}
\usepackage[authoryear,longnamesfirst,sort]{natbib}
\bibpunct();A{},

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\ttdefault}{cmtt} % CM rather than courier for \tt

% for uniform font size
\renewcommand{\isastyle}{\isastyleminor}

% Abstract various things that might change.
\newcommand{\ccode}[1]{\texttt{#1}}
\newcommand{\isabelletype}[1]{\emph{#1}}
\newcommand{\isabelleterm}[1]{\emph{#1}}

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

\begin{document}

\title{Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO}
\author{Peter Gammie, Tony Hosking and Kai Engelhardt}
\maketitle

\begin{abstract}
  We model an instance of Schism, a state-of-the-art real-time garbage
  collection scheme for weak memory, and show that it is safe on
  x86-TSO.
\end{abstract}

\tableofcontents

\section{Introduction}
\label{sec:introduction}

We verify the memory safety of one of the Schism garbage collectors as
developed by \citet{Pizlo+2010PLDI,Pizlo201xPhd} with respect to the
x86-TSO model (a total store order memory model for modern multicore
Intel x86 architectures) developed and validated by
\citet{DBLP:journals/cacm/SewellSONM10}.

Our development is inspired by the original work on the verification
of concurrent mark/sweep collectors by
\citet{DBLP:journals/cacm/DijkstraLMSS78}, and the more realistic
models and proofs of \citet{DoligezGonthier:1994}. We leave a thorough
survey of formal garbage collection verification to future work.

We present our model of the garbage collector in \S\ref{sec:gc-model},
the predicates we use in our assertions in \S\ref{sec:proofs-basis},
the detailed invariants in \S\ref{sec:global-invariants} and
\S\ref{sec:local-invariants}, and the high-level safety results in
\S\ref{sec:top-level-correctness}. A concrete system state that
satisfies our invariants is exhibited in
\S\ref{sec:concrete-system-state}. The other sections contain the
often gnarly proofs and lemmas starring in supporting roles.

The modelling language CIMP used in this development is described in
the AFP entry ConcurrentIMP \citep{ConcurrentIMP_AFP}.


% generated text of all theories
\input{session}

\bibliographystyle{plainnat}
\bibliography{root}
\addcontentsline{toc}{section}{References}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
