1% 2% Copyright 2014, General Dynamics C4 Systems 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(GD_GPL) 9% 10 11% LaTeX master document for abstract spec. 12 13\documentclass[10pt,a4paper]{scrbook} 14 15% These old font commands have been removed from newer versions of 16% the scrbook document class, but isabelle.sty still uses them. 17\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm} 18\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf} 19\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt} 20\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf} 21\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit} 22\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl} 23\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc} 24 25\usepackage{isabelle,isabellesym} 26 27% further packages required for unusual symbols (see also isabellesym.sty) 28% use only when needed 29\usepackage{amssymb} % for \<leadsto>, \<box>, \<diamond>, 30 % \<sqsupset>, \<mho>, \<Join>, 31 % \<lhd>, \<lesssim>, \<greatersim>, 32 % \<lessapprox>, \<greaterapprox>, 33 % \<triangleq>, \<yen>, \<lozenge> 34\usepackage[english]{babel} % greek for \<euro>, 35 % english for \<guillemotleft>, 36 % \<guillemotright> 37 % default language = last 38%\usepackage[latin1]{inputenc} % for \<onesuperior>, \<onequarter>, 39 % \<twosuperior>, \<onehalf>, 40 % \<threesuperior>, \<threequarters>, 41 % \<degree> 42%\usepackage[only,bigsqcap]{stmaryrd} % for \<Sqinter> 43%\usepackage{eufrak} % for \<AA> ... \<ZZ>, \<aa> ... \<zz> 44 % (only needed if amssymb not used) 45 46\usepackage{graphicx} 47\usepackage[draft]{fixme} 48\usepackage{cite} 49\usepackage{xspace} 50 51% this should be the last package used 52\usepackage{color} 53\definecolor{linkcolor}{rgb}{0,0,0.7} 54\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor, 55 filecolor=linkcolor,pagecolor=linkcolor,urlcolor=linkcolor]{hyperref} 56 57\urlstyle{rm} 58\isabellestyle{tt} 59 60\newcommand{\version}{\input{VERSION}\xspace} 61\newcommand{\arch}{\input{ARCH}\xspace} 62\newcommand{\gitrev}{\input{gitrev}\xspace} 63 64\hypersetup 65{ 66 pdfauthor={Trustworthy Systems, Data61}, 67 pdftitle={Abstract Formal Specification of the seL4/\arch API} 68} 69 70\renewcommand{\isamarkupchapter}[1]{\chapter{#1}} 71 72% don't show ML code 73\isadroptag{ML} 74 75% don't show proofs 76\isadroptag{proof} 77 78% do not show confusing double quotes in definitions and lemmas 79%\renewcommand{\isachardoublequote}{} 80%\renewcommand{\isachardoublequoteopen}{} 81%\renewcommand{\isachardoublequoteclose}{} 82 83\parindent 0pt\parskip 0.5ex 84 85\setlength{\oddsidemargin}{0cm} 86\setlength{\evensidemargin}{0cm} 87\setlength{\topmargin}{-1cm} 88\setlength{\textwidth}{15.5cm} 89\setlength{\textheight}{22.5cm} 90 91\newcommand{\meth}[1]{\texttt{#1()}} 92\newcommand{\obj}[1]{\textsf{\small #1}} 93 94\begin{document} 95 96\title{Abstract Formal Specification of the seL4/\arch API} 97 98\date{Version \version} 99 100\author{% 101June Andronick \and 102Joel Beeren \and 103Matthew Brecknell \and 104Timothy Bourke \and 105Philip Derrin \and 106Kevin Elphinstone \and 107Xin Gao \and 108David Greenaway \and 109Alejandro Gomez-Londono \and 110Gerwin Klein \and 111Rafal Kolanski \and 112Ramana Kumar \and 113Daniel Matichuk \and 114Thomas Sewell \and 115Michael Sproul \and 116Miki Tanaka \and 117Sophie Taylor \and 118Simon Winwood 119} 120 121\maketitle 122 123\thispagestyle{empty} 124 125\vfill 126 127\copyright~2014 National ICT Australia Limited.\\ 128\copyright~2014 Open Kernel Labs, Inc.\\ 129\copyright~2018 Data61, CSIRO.\\ 130 131\textsc{All rights reserved}. 132 133\bigskip 134 135Architecture: \arch\\ 136Document build date: \today\\ 137Produced from git change set: \gitrev 138 139\clearpage 140 141\chapter*{Abstract} 142This document is the text version of the abstract, formal 143Isabelle/HOL specification of the seL4 microkernel. It is 144intended to give a precise, operational definition of the 145seL4 microkernel on the \arch architecture. 146The document contains a short overview, followed by 147text generated from the formal Isabelle/HOL definitions. 148 149This document is not a tutorial or user manual and is not intended to be read 150as such. Please see the bundled user manual for a higher-level introduction to 151the kernel. 152 153 154\cleardoublepage 155 156\tableofcontents 157 158\input{session} 159 160\bibliographystyle{plain} 161\bibliography{defs,root} 162 163\end{document} 164 165%%% Local Variables: 166%%% mode: latex 167%%% TeX-master: t 168%%% End: 169