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,component,composition,connection,control,consumes,dataport,emits,event,from,in,inout,int,out,procedure,provides,smallstring,to,uses}}\lstinputlisting{#1}}}
63
64
65\ifDraft
66\usepackage{draftcopy}
67\newcommand{\Comment}[1]{\textbf{\textsl{#1}}}
68\newcommand{\FIXME}[1]{\textbf{\textsl{FIXME: #1}}}
69\newcommand{\todo}[1]{\textbf{TODO: \textsl{#1}}}
70\date{\small\today}
71\else
72\newcommand{\Comment}[1]{\relax}
73\newcommand{\FIXME}[1]{\relax}
74\newcommand{\todo}[1]{\relax}
75\date{}
76\fi
77
78
79% From camkes manual
80\newcommand{\selfour}{seL4\xspace}
81\newcommand{\Selfour}{SeL4\xspace}
82\newcommand{\camkes}{CAmkES\xspace}
83
84\newcommand{\code}[1]{\texttt{#1}}
85
86
87\newcommand{\titl}{CAmkES Glue Code Semantics}
88\newcommand{\authors}{Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein, Ihor Kuz}
89
90\definecolor{lcol}{rgb}{0,0,0.5}
91\usepackage[bookmarks,hyperindex,pdftex,
92            colorlinks=true,linkcolor=lcol,citecolor=lcol,
93            filecolor=lcol,urlcolor=lcol,
94            pdfauthor={\authors},
95            pdftitle={\titl},
96            plainpages=false]{hyperref}
97
98
99\addto\extrasenglish{%
100\renewcommand{\chapterautorefname}{Chapter}
101\renewcommand{\sectionautorefname}{Section}
102\renewcommand{\subsectionautorefname}{Section}
103\renewcommand{\subsubsectionautorefname}{Section}
104\renewcommand{\appendixautorefname}{Appendix}
105\renewcommand{\Hfootnoteautorefname}{Footnote}
106}
107
108% urls in roman style
109\urlstyle{rm}
110
111\lstset{basicstyle=\small\tt}
112
113% isabelle style
114\isabellestyle{tt}
115
116% for uniform isabelle font size
117\renewcommand{\isastyle}{\isastyleminor}
118
119% Abstract various things that might change.
120\newcommand{\ccode}[1]{\texttt{#1}}
121\newcommand{\isabelletype}[1]{\emph{#1}}
122\newcommand{\isabelleterm}[1]{\emph{#1}}
123
124\renewcommand{\isamarkupheader}[1]{\chapter{#1}}
125\renewcommand{\isamarkupchapter}[1]{\chapter{#1}}
126\renewcommand{\isamarkupsection}[1]{\section{#1}}
127\renewcommand{\isamarkupsubsection}[1]{\section{#1}}
128\renewcommand{\isamarkupsubsubsection}[1]{\subsection{#1}}
129
130\newcommand{\nictafundingacknowledgement}{%
131% Lifted from http://wiki.inside.nicta.com.au/display/CHNOPSR/Funding+Acknowledgement 28-10-2013
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
136\newcommand{\cpright}{Copyright \copyright\ 2013 NICTA, \ABN.  All rights reserved.}
137\newcommand{\disclaimer}{%
138\cpright}
139
140\newcommand{\trdisclaimer}{%
141This material is based on research sponsored by Air Force Research Laboratory
142and the Defense Advanced Research Projects Agency (DARPA) under agreement number
143FA8750-12-9-0179. The U.S. Government is authorized to reproduce and distribute
144reprints for Governmental purposes notwithstanding any copyright notation
145thereon.
146
147The views and conclusions contained herein are those of the authors and should
148not be interpreted as necessarily representing the official policies or
149endorsements, either expressed or implied, of Air Force Research Laboratory,
150the Defense Advanced Research Projects Agency or the U.S.Government.}
151
152\newcommand{\smalldisclaimer}{}
153\newcommand{\bigdisclaimer}{%
154\nictafundingacknowledgement\\
155
156\cpright\\
157
158\vspace{2ex}
159\noindent\trdisclaimer}
160
161\newcommand{\pgstyle}{%
162\fancyhf{}%
163\renewcommand{\headrulewidth}{0pt}%
164\fancyfoot[C]{}%
165\fancyfoot[L]{\smalldisclaimer}%
166\fancyfoot[R]{\sl\thepage}}
167
168\fancypagestyle{plain}{\pgstyle}
169
170
171\begin{document}
172
173\parindent 0pt\parskip 0.5ex plus 0.2ex minus 0.1ex
174
175%--------- title page
176\newgeometry{left=25mm,right=25mm,top=35mm,bottom=35mm}
177
178\begin{center}
179 \includegraphics[width=0.2\textwidth]{imgs/NICTA_logo}
180\end{center}
181
182\vspace{14ex}
183\textsf{\huge \titl}
184
185%\vspace{2ex}
186%\textsf{\huge \subtitl}
187
188\vspace{4ex}
189\rule{0.85\textwidth}{5pt}
190\vspace{4ex}
191
192{\large \authors
193
194\vspace{2ex}
195April 2013}
196
197\vfill
198{\small
199\bigdisclaimer
200}
201
202\thispagestyle{empty}
203\newpage
204~
205\restoregeometry
206
207\fancypagestyle{empty}{\pgstyle}
208\pagestyle{empty}
209
210%--------- end title page
211
212\cleardoublepage
213
214\chapter*{Abstract}
215
216This document describes the formal dynamic semantics of \camkes glue code, in
217particular of the communication stubs generated for components at compile
218time. The semantics is based on a simple concurrent imperative language with
219message passing that is easy to extend and instantiate for specific
220applications. Instead of one generic semantics for all systems, we take the
221approach of generating a high-level semantic description for each specific
222ADL component specification to ease verification of specific systems in
223the future.
224
225We show the definitions and types for expressing components and glue code, and
226provide some examples of generated Isabelle theories with synchronous,
227asynchronous, and shared memory communication.
228
229
230\cleardoublepage
231\tableofcontents
232
233\input{intro}
234
235% generated text of all theories
236\input{session}
237
238% optional bibliography
239\bibliographystyle{plain}
240\bibliography{root}
241
242\end{document}
243