1%
2% Copyright 2014, NICTA
3%
4% This software may be distributed and modified according to the terms of
5% the GNU General Public License version 2. Note that NO WARRANTY is provided.
6% See "LICENSE_GPLv2.txt" for details.
7%
8% @TAG(NICTA_GPL)
9%
10
11\documentclass[11pt,a4paper]{scrreprt}
12
13% These old font commands have been removed from newer versions of
14% the scrreprt document class, but isabelle.sty still uses them.
15\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
16\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
17\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
18\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
19\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
20\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl}
21\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc}
22
23\newif \ifDraft         \Draftfalse
24
25\usepackage{isabelle,isabellesym}
26
27% further packages required for unusual symbols (see also
28% isabellesym.sty), use only when needed
29
30%\usepackage{amssymb}
31  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
32  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
33  %\<triangleq>, \<yen>, \<lozenge>
34
35\usepackage[english]{babel}
36  %option greek for \<euro>
37  %option english (default language) for \<guillemotleft>, \<guillemotright>
38
39%\usepackage[only,bigsqcap]{stmaryrd}
40  %for \<Sqinter>
41
42%\usepackage{eufrak}
43  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
44
45%\usepackage{textcomp}
46  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
47  %\<currency>
48
49
50% Extra CAmkES bits.
51\usepackage{graphicx}
52\usepackage{enumerate}
53
54% From ERTOS setup
55\setkeys{Gin}{keepaspectratio=true,clip=true,draft=false,width=\linewidth}
56\usepackage{times,cite,url,fancyhdr,microtype,color,geometry}
57
58\renewcommand{\ttdefault}{cmtt}        % CM rather than courier for \tt
59
60\usepackage{xspace}
61\usepackage{listings}
62\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}}}
63\newcommand{\clisting}[1]{{\lstset{language=C,basicstyle=\small\ttfamily,keywordstyle=\bf}\lstinputlisting{#1}}}
64
65
66\ifDraft
67\usepackage{draftcopy}
68\newcommand{\Comment}[1]{\textbf{\textsl{#1}}}
69\newcommand{\FIXME}[1]{\textbf{\textsl{FIXME: #1}}}
70\newcommand{\todo}[1]{\textbf{TODO: \textsl{#1}}}
71\date{\small\today}
72\else
73\newcommand{\Comment}[1]{\relax}
74\newcommand{\FIXME}[1]{\relax}
75\newcommand{\todo}[1]{\relax}
76\date{}
77\fi
78
79
80% From camkes manual
81\newcommand{\selfour}{seL4\xspace}
82\newcommand{\Selfour}{SeL4\xspace}
83\newcommand{\camkes}{CAmkES\xspace}
84
85\newcommand{\code}[1]{\texttt{#1}}
86
87
88\newcommand{\titl}{CAmkES Glue Code Proofs}
89\newcommand{\authors}{Matthew Fernandez, June Andronick, Gerwin Klein, Ihor Kuz}
90
91\definecolor{lcol}{rgb}{0,0,0.5}
92\usepackage[bookmarks,hyperindex,pdftex,
93            colorlinks=true,linkcolor=lcol,citecolor=lcol,
94            filecolor=lcol,urlcolor=lcol,
95            pdfauthor={\authors},
96            pdftitle={\titl},
97            plainpages=false]{hyperref}
98
99
100\addto\extrasenglish{%
101\renewcommand{\chapterautorefname}{Chapter}
102\renewcommand{\sectionautorefname}{Section}
103\renewcommand{\subsectionautorefname}{Section}
104\renewcommand{\subsubsectionautorefname}{Section}
105\renewcommand{\appendixautorefname}{Appendix}
106\renewcommand{\Hfootnoteautorefname}{Footnote}
107}
108
109% urls in roman style
110\urlstyle{rm}
111
112\lstset{basicstyle=\small\tt}
113
114% isabelle style
115\isabellestyle{tt}
116
117% for uniform isabelle font size
118\renewcommand{\isastyle}{\isastyleminor}
119
120% Abstract various things that might change.
121\newcommand{\ccode}[1]{\texttt{#1}}
122\newcommand{\isabelletype}[1]{\emph{#1}}
123\newcommand{\isabelleterm}[1]{\emph{#1}}
124
125\renewcommand{\isamarkupheader}[1]{\chapter{#1}}
126\renewcommand{\isamarkupchapter}[1]{\chapter{#1}}
127\renewcommand{\isamarkupsection}[1]{\section{#1}}
128\renewcommand{\isamarkupsubsection}[1]{\section{#1}}
129\renewcommand{\isamarkupsubsubsection}[1]{\subsection{#1}}
130
131\newcommand{\nictafundingacknowledgement}{%
132NICTA 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.}
133
134\newcommand{\ABN}{ABN 62 102 206 173}
135\newcommand{\addr}{Level 5, 13 Garden Street, Eveleigh, New South Wales,
136Australia}
137
138\newcommand{\cpright}{Copyright \copyright\ 2014 NICTA, \ABN.  All rights reserved.}
139
140\newcommand{\bigdisclaimer}{%
141\nictafundingacknowledgement\\
142
143\cpright}
144
145\newcommand{\pgstyle}{%
146\fancyhf{}%
147\renewcommand{\headrulewidth}{0pt}%
148\fancyfoot[C]{}%
149\fancyfoot[L]{}%
150\fancyfoot[R]{\sl\thepage}}
151
152\fancypagestyle{plain}{\pgstyle}
153
154
155\begin{document}
156
157\parindent 0pt\parskip 0.5ex plus 0.2ex minus 0.1ex
158
159%--------- title page
160\newgeometry{left=25mm,right=25mm,top=35mm,bottom=35mm}
161
162\begin{center}
163 \includegraphics[width=0.2\textwidth]{imgs/NICTA_logo}
164\end{center}
165
166\vspace{14ex}
167\textsf{\huge \titl}
168
169%\vspace{2ex}
170%\textsf{\huge \subtitl}
171
172\vspace{4ex}
173\rule{0.85\textwidth}{5pt}
174\vspace{4ex}
175
176{\large \authors
177
178\vspace{2ex}
179May 2014}
180
181\vfill
182{\small
183\bigdisclaimer
184}
185
186\thispagestyle{empty}
187\newpage
188~
189\restoregeometry
190
191\fancypagestyle{empty}{\pgstyle}
192\pagestyle{empty}
193
194%--------- end title page
195
196\cleardoublepage
197
198\chapter*{Abstract}
199
200This document describes desirable correctness properties of the \camkes glue
201code and the automated process for generating proofs of these properties.
202Sample generated proofs are shown for simple component systems to exemplify the
203style of these proofs and the relationship they bear to the generated code.
204This code, that performs communication between component instances, is
205abstracted to a monadic representation on which the proofs are then generated.
206The proven properties are guaranteed to hold on the generated code, under the
207assumption that the abstraction steps are correct.
208We consider this assumption reasonable, as the abstraction steps consist of a
209minimal translation of C code into an interactive theorem prover, followed by further
210proof-producing transformations.
211
212This report covers synchronous, asynchronous and shared memory communication in
213\camkes and is intended to extend the previous reports on the formalisation of
214the \camkes platform.
215
216\cleardoublepage
217\tableofcontents
218
219\input{intro}
220
221% generated text of all theories
222\input{session}
223
224% optional bibliography
225\bibliographystyle{plain}
226\bibliography{root}
227
228\end{document}
229