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