%
% Copyright 2014, NICTA
%
% This software may be distributed and modified according to the terms of
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
% See "LICENSE_GPLv2.txt" for details.
%
% @TAG(NICTA_GPL)
%

\documentclass[11pt,a4paper]{scrreprt}

% These old font commands have been removed from newer versions of
% the scrreprt document class, but isabelle.sty still uses them.
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl}
\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc}

\newif \ifDraft         \Draftfalse

\usepackage{isabelle,isabellesym}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

%\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

\usepackage[english]{babel}
  %option greek for \<euro>
  %option english (default language) for \<guillemotleft>, \<guillemotright>

%\usepackage[only,bigsqcap]{stmaryrd}
  %for \<Sqinter>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>


% Extra CAmkES bits.
\usepackage{graphicx}
\usepackage{enumerate}

% From ERTOS setup
\setkeys{Gin}{keepaspectratio=true,clip=true,draft=false,width=\linewidth}
\usepackage{times,cite,url,fancyhdr,microtype,color,geometry}

\renewcommand{\ttdefault}{cmtt}        % CM rather than courier for \tt

\usepackage{xspace}
\usepackage{listings}
\newcommand{\camkeslisting}[1]{{\lstset{basicstyle=\small\ttfamily,keywordstyle=\bf,morekeywords={assembly,char,component,composition,connection,control,consumes,dataport,emits,event,from,in,inout,int,out,procedure,provides,smallstring,to,uint64_t,uses,void}}\lstinputlisting{#1}}}
\newcommand{\clisting}[1]{{\lstset{language=C,basicstyle=\small\ttfamily,keywordstyle=\bf}\lstinputlisting{#1}}}


\ifDraft
\usepackage{draftcopy}
\newcommand{\Comment}[1]{\textbf{\textsl{#1}}}
\newcommand{\FIXME}[1]{\textbf{\textsl{FIXME: #1}}}
\newcommand{\todo}[1]{\textbf{TODO: \textsl{#1}}}
\date{\small\today}
\else
\newcommand{\Comment}[1]{\relax}
\newcommand{\FIXME}[1]{\relax}
\newcommand{\todo}[1]{\relax}
\date{}
\fi


% From camkes manual
\newcommand{\selfour}{seL4\xspace}
\newcommand{\Selfour}{SeL4\xspace}
\newcommand{\camkes}{CAmkES\xspace}

\newcommand{\code}[1]{\texttt{#1}}


\newcommand{\titl}{CAmkES Glue Code Proofs}
\newcommand{\authors}{Matthew Fernandez, June Andronick, Gerwin Klein, Ihor Kuz}

\definecolor{lcol}{rgb}{0,0,0.5}
\usepackage[bookmarks,hyperindex,pdftex,
            colorlinks=true,linkcolor=lcol,citecolor=lcol,
            filecolor=lcol,urlcolor=lcol,
            pdfauthor={\authors},
            pdftitle={\titl},
            plainpages=false]{hyperref}


\addto\extrasenglish{%
\renewcommand{\chapterautorefname}{Chapter}
\renewcommand{\sectionautorefname}{Section}
\renewcommand{\subsectionautorefname}{Section}
\renewcommand{\subsubsectionautorefname}{Section}
\renewcommand{\appendixautorefname}{Appendix}
\renewcommand{\Hfootnoteautorefname}{Footnote}
}

% urls in roman style
\urlstyle{rm}

\lstset{basicstyle=\small\tt}

% isabelle style
\isabellestyle{tt}

% for uniform isabelle 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}}

\renewcommand{\isamarkupheader}[1]{\chapter{#1}}
\renewcommand{\isamarkupchapter}[1]{\chapter{#1}}
\renewcommand{\isamarkupsection}[1]{\section{#1}}
\renewcommand{\isamarkupsubsection}[1]{\section{#1}}
\renewcommand{\isamarkupsubsubsection}[1]{\subsection{#1}}

\newcommand{\nictafundingacknowledgement}{%
NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program. NICTA is also funded and supported by the Australian Capital Territory, the New South Wales, Queensland and Victorian Governments, the Australian National University, the University of New South Wales, the University of Melbourne, the University of Queensland, the University of Sydney, Griffith University, Queensland University of Technology, Monash University and other university partners.}

\newcommand{\ABN}{ABN 62 102 206 173}
\newcommand{\addr}{Level 5, 13 Garden Street, Eveleigh, New South Wales,
Australia}

\newcommand{\cpright}{Copyright \copyright\ 2014 NICTA, \ABN.  All rights reserved.}

\newcommand{\bigdisclaimer}{%
\nictafundingacknowledgement\\

\cpright}

\newcommand{\pgstyle}{%
\fancyhf{}%
\renewcommand{\headrulewidth}{0pt}%
\fancyfoot[C]{}%
\fancyfoot[L]{}%
\fancyfoot[R]{\sl\thepage}}

\fancypagestyle{plain}{\pgstyle}


\begin{document}

\parindent 0pt\parskip 0.5ex plus 0.2ex minus 0.1ex

%--------- title page
\newgeometry{left=25mm,right=25mm,top=35mm,bottom=35mm}

\begin{center}
 \includegraphics[width=0.2\textwidth]{imgs/NICTA_logo}
\end{center}

\vspace{14ex}
\textsf{\huge \titl}

%\vspace{2ex}
%\textsf{\huge \subtitl}

\vspace{4ex}
\rule{0.85\textwidth}{5pt}
\vspace{4ex}

{\large \authors

\vspace{2ex}
May 2014}

\vfill
{\small
\bigdisclaimer
}

\thispagestyle{empty}
\newpage
~
\restoregeometry

\fancypagestyle{empty}{\pgstyle}
\pagestyle{empty}

%--------- end title page

\cleardoublepage

\chapter*{Abstract}

This document describes desirable correctness properties of the \camkes glue
code and the automated process for generating proofs of these properties.
Sample generated proofs are shown for simple component systems to exemplify the
style of these proofs and the relationship they bear to the generated code.
This code, that performs communication between component instances, is
abstracted to a monadic representation on which the proofs are then generated.
The proven properties are guaranteed to hold on the generated code, under the
assumption that the abstraction steps are correct.
We consider this assumption reasonable, as the abstraction steps consist of a
minimal translation of C code into an interactive theorem prover, followed by further
proof-producing transformations.

This report covers synchronous, asynchronous and shared memory communication in
\camkes and is intended to extend the previous reports on the formalisation of
the \camkes platform.

\cleardoublepage
\tableofcontents

\input{intro}

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{plain}
\bibliography{root}

\end{document}
