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