manual: Purely cosmetic changes / improved wording

.gitignore

@@ -29,3 +29,6 @@ manual/manual.pdf
 libsel4/arch_include/arm/sel4/arch/invocation.h
 libsel4/arch_include/ia32/sel4/arch/invocation.h
 libsel4/arch_include/x86/sel4/arch/invocation.h
+
+# Emacs backups
+*~

manual/disy.sty

@@ -67,7 +67,7 @@
 \newcommand{\AuthorEmail}[1]{\def\AuthorEmailString{#1}}
 
 \newcommand{\CrestFileName}{\ifColor unicrest-colour\else unicrest-screen\fi}
-%\newcommand{\LogoFileName}{\ifColor nicta-col\else nicta-bw\fi}
+\newcommand{\LogoFileName}{nicta-col}
 \AuthorEmail{disy@cse.unsw.edu.au}
 
 \newlength{\centeroffset}
@@ -91,25 +91,25 @@
       \newlength{\ERTOSw}%
       %\setlength{\ERTOSw}{\textwidth}%
       %\addtolength{\ERTOSw}{-\LogoW}\addtolength{\ERTOSw}{-2em}%
-      \settowidth{\ERTOSw}{{\sf\large http://ssrg.nicta.com.au/}}%
+      \settowidth{\ERTOSw}{{\sf\large http://ssrg.nicta.com.au/projects/TS/}}%
       %\settowidth{\ERTOSw}{{\sf\large Operating Systems Group}}%
-      %\newcommand{\NICTAlogo}{\includegraphics[width=\LogoW]{imgs/\LogoFileName}}%
+      \newcommand{\NICTAlogo}{\includegraphics[width=\LogoW]{figs/\LogoFileName}}%
       \noindent\sf%
       \begin{minipage}[b]{\textwidth}\sf\large%
 	\hspace*{-10mm}%
 	\ifNICTA%
 	  \color{nictablue}%
-          \begin{minipage}[b]{1.1\ERTOSw}\urlstyle{sf}%
-            Trustworthy Systems\\
- 	  \url{http://ssrg.nicta.com.au/}\\~
+          \begin{minipage}[b]{\ERTOSw}\urlstyle{sf}%
+            NICTA Trustworthy Systems\\
+ 	  \url{http://ssrg.nicta.com.au/projects/TS/}\\~
 	  \end{minipage}
 	  \hfill
-%	  \ifx\undefined\hyperref%
-%	    \NICTAlogo%
-% 	  \else%
-%	    \raisebox{2mm}{\href{http://nicta.com.au}{\NICTAlogo}}%
-%	  \fi%
-%	\else~
+	  \ifx\undefined\hyperref%
+	    \NICTAlogo%
+ 	  \else%
+	    \raisebox{2mm}{\href{http://nicta.com.au}{\NICTAlogo}}%
+	  \fi%
+	\else~
 	\fi%
       \end{minipage}%
       \hspace*{-4mm}%

manual/manual.tex

@@ -13,6 +13,7 @@
 
 % Setting this to true turns on the `draft' watermark
 \newif \ifDraft \Draftfalse
+\Drafttrue
 
 \newif \ifxeightsix   \xeightsixtrue
 

manual/parts/api/untyped_retype.tex

@@ -93,7 +93,7 @@ and~\ref{tab:arm_obj_sizes}.
                 \bottomrule
             \end{tabular}
         \end{center}
-    \caption{Platform Independent Object Sizes}
+    \caption{Platform-independent object sizes.}
     \label{tab:obj_sizes}
 \end{table}
 
@@ -118,7 +118,7 @@ and~\ref{tab:arm_obj_sizes}.
                 \bottomrule
             \end{tabular}
         \end{center}
-    \caption{IA-32 Specific Object Sizes}
+    \caption{IA-32-specific object sizes.}
     \label{tab:intel_obj_sizes}
     }
 \hfill
@@ -141,7 +141,7 @@ and~\ref{tab:arm_obj_sizes}.
                 \bottomrule
             \end{tabular}
         \end{center}
-    \caption{ARM Specific Object Sizes}
+    \caption{ARM-specific object sizes.}
     \label{tab:arm_obj_sizes}
     }
 \end{table}

manual/parts/bootup.tex

@@ -29,7 +29,7 @@ The first 12 slots contain specific capabilities as listed in
 
 \begin{table}[htb]
   \begin{center}
-    \caption{Initial Thread's CNode Content}
+    \caption{Initial thread's CNode content.}
     \label{tab:cnode_content}
     \begin{tabularx}{\textwidth}{llX}
       \toprule
@@ -85,7 +85,7 @@ of slots in the initial thread's CNode, starting with CPTR \texttt{start} and wi
 
 \begin{table}[htb]
   \begin{center}
-    \caption{BootInfo Struct}
+    \caption{BootInfo struct.}
     \label{tab:bootinfo_struct}
     \begin{tabularx}{\textwidth}{llX}
       \toprule
@@ -135,7 +135,7 @@ provides a compile-time-configurable minimum number of 4K untyped capabilities
 
 \begin{table}[htb]
   \begin{center}
-    \caption{DeviceRegion Struct}
+    \caption{DeviceRegion struct.}
     \label{tab:device_region_struct}
     \begin{tabular}{lll}
       \toprule
@@ -186,7 +186,7 @@ Arguments are listed in \autoref{tab:bootargs} along with their default values (
 
 
 \begin{table}[htb]
-    \caption{IA-32 boot command-line arguments}
+    \caption{IA-32 boot command-line arguments.}
         \begin{tabularx}{\textwidth}{lXX}
             \toprule
               Key & Value & Default \\

manual/parts/cspace.tex

@@ -187,7 +187,7 @@ derived once.
     \obj{IO Page Table (IA-32 only)} & Must be mapped & \enummem{seL4\_IllegalOperation}\\
     \fi \bottomrule
   \end{tabularx}
-  \caption{Capability Derivation\label{tab:cap-derivation}}
+  \caption{Capability derivation.\label{tab:cap-derivation}}
 \end{table}
 
 \begin{figure}[th]
@@ -404,7 +404,7 @@ in this CSpace.
 \begin{figure}[tb]
   \begin{center}
     \includegraphics[scale=0.5]{figs/fig2-1.pdf}
-    \caption{An arbitrary CSpace layout}
+    \caption{An arbitrary CSpace layout.}
     \label{fig2.1}
   \end{center}
 \end{figure}

manual/parts/intro.tex

@@ -20,7 +20,13 @@ spaces, threads, and inter-process communication (IPC). The small number
 of services provided by seL4 directly translates to a small
 implementation of approximately $8700$ lines of C code. This has allowed
 the ARMv6 version of the kernel to be formally proven in the Isabelle/HOL 
-theorem prover to adhere to its formal specification~\cite{Boyton_09,Cock_KS_08,Derrin_EKCC_06,Elkaduwe_GE_08,Klein_EHACDEEKNSTW_09,Tuch_KN_07,Winwood_KSACN_09}.
+theorem prover to adhere to its formal
+specification~\cite{Boyton_09,Cock_KS_08,Derrin_EKCC_06,Elkaduwe_GE_08,Klein_EHACDEEKNSTW_09,Tuch_KN_07,Winwood_KSACN_09},
+which in turn enabled proofs of the kernel's enforcement of
+integrity~\cite{Sewell_WGMAK_11} and
+confidentiality~\cite{Murray_MBGBSLGK_13}. The kernel's small size was
+also instrumental in performing a complete and sound analysis of
+worst-case execution time~\cite{Blackham_SCRH_11,Blackham_SH_12}.
 
 This manual describes the seL4 kernel's API from a user's point of view.
 The document starts by giving a brief overview of the seL4 microkernel

manual/parts/objects.tex

@@ -64,7 +64,7 @@ may not contain a capability.  An application may refer to
 a capability---to request a kernel service, for example---using the
 address of the slot holding that capability.  This means, the seL4 
 capability model is an instance of a \emph{segregated} (or \emph{partitioned})
-capability model, where capabilities are managed by the kernel.
+capability system, where capabilities are managed by the kernel.
 
 Capability spaces are implemented as a directed graph of kernel-managed
 \emph{capability nodes} (\obj{CNode}s).  A \obj{CNode} is a table of
@@ -212,9 +212,8 @@ manipulation, and combination of these kernel objects:
     \item[Virtual Address Space Objects] (see \autoref{ch:vspace}) 
     are used to construct a virtual
     address space (or VSpace) for one or more threads. These
-    objects largely directly correspond to those of the hardware; that
-    is, a page directory pointing to page tables, which in turn map
-    physical frames. The kernel also includes \obj{ASID
+    objects largely directly correspond to those of the hardware, and
+    as such are architecture-dependent. The kernel also includes \obj{ASID
     Pool} and \obj{ASID Control} objects for tracking the status of
     address spaces.
 
@@ -244,10 +243,10 @@ manipulation, and combination of these kernel objects:
 \label{sec:kernmemalloc}
 
 The seL4 microkernel does not dynamically allocate memory for kernel objects.
-Kernel objects must be explicitly created from application-controlled memory
+Instead, objects must be explicitly created from application-controlled memory
 regions via \obj{Untyped Memory} capabilities.  Applications must have
 explicit authority to memory (through these \obj{Untyped Memory} capabilities) in
-order to create new objects, and all objects consume constant memory once
+order to create new objects, and all objects consume a fixed amount of memory once
 created. These mechanisms can be used to precisely control
 the specific amount of physical memory available to applications,
 including being able to enforce isolation of physical memory access
@@ -260,7 +259,9 @@ exhaustion are avoided.
 
 At boot time, seL4 pre-allocates the memory required for the kernel
 itself, including the code, data, and stack sections (seL4 is a single
-kernel-stack operating system). The remainder of the memory is given to
+kernel-stack operating system). It then creates an initial user
+thread (with an appropriate address and capability space).
+The kernel than hands all remaining memory to
 the initial thread in the form of capabilities to \obj{Untyped Memory}, and
 some additional capabilities to kernel objects that were required to
 bootstrap the initial thread.  These \obj{Untyped Memory} regions can then be split into
@@ -299,7 +300,7 @@ capabilities would be inserted into the CDT as children of the untyped
 memory capability.
 
 For each \obj{Untyped Memory} region, the kernel keeps
-a \emph{watermark} recording how much of region has previously been
+a \emph{watermark} recording how much of the region has previously been
 allocated. Whenever a user requests the kernel to create new objects in
 an untyped memory region, the kernel will carry out one of two actions:
 if there are already existing objects allocated in the region, the

manual/parts/threads.tex

@@ -67,11 +67,11 @@ set with \apifunc{seL4\_TCB\_Configure}{tcb_configure} and
 
 Each thread has an associated exception-handler endpoint. If the thread
 causes an exception, the kernel creates an IPC message with the relevant
-details and forwards this to a thread waiting on the endpoint. This
+details and sends this to the endpoint. This
 thread can then take the appropriate action. Fault IPC messages are
 described in \autoref{sec:faults}.
 
-In order to enable exception handlers a capability to the exception-handler
+In order to enable exception handlers, a capability to the exception-handler
 endpoint must exist in the CSpace of the thread that generates the exception.
 The exception-handler
 endpoint can be set with the \apifunc{seL4\_TCB\_SetSpace}{tcb_setspace} or
@@ -84,7 +84,7 @@ when an exception actually happens and if the lookup fails then no
 exception message is delivered and the thread is suspended indefinitely.
 
 The exception endpoint must have send and grant rights. Replying to the
-IPC restarts the thread. For certain exception types, the contents of
+exception message restarts the thread. For certain exception types, the contents of
 the reply message may be used to set the values in the registers of the
 thread being restarted.
 See \autoref{sec:faults} for details.
@@ -170,7 +170,7 @@ IPC message are given in \autoref{tbl:ipc_contents}.\\
 \toprule
 \textbf{Meaning} & \textbf{IPC buffer Location} \\
 \midrule
-Program counter to restart execution at & \ipcbloc{IPCBuffer[0]} \\
+Address at which to restart execution & \ipcbloc{IPCBuffer[0]} \\
 Capability address & \ipcbloc{IPCBuffer[1]}\\
 In receive phase (1 if the fault happened during a wait system call, 0
 otherwise) & \ipcbloc{IPCBuffer[2]}\\

manual/parts/vspace.tex

@@ -31,7 +31,7 @@ capabilities to the required objects.
 IA-32 processors have a two-level page-table structure.
 The top-level page directory covers a 4\,GiB range and each page table covers a 4\,MiB range.
 Frames can be 4\,KiB or 4\,MiB.
-Before a 4KiB
+Before a 4\,KiB
 frame can be mapped, a page table covering the range that the frame will
 be mapped into must have been mapped, otherwise seL4 will return an
 error.

manual/references.bib

@@ -13,6 +13,26 @@ THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT!
 |  BIBTEX ENTRIES   |
 `-------------------'
 
+  @inproceedings{Blackham_SCRH_11,
+    author           = {Blackham, Bernard and Shi, Yao and Chattopadhyay, Sudipta and Roychoudhury, Abhik and Heiser, Gernot},
+    month            = nov,
+    pages            = {339-348},
+    year             = {2011},
+    title            = {Timing Analysis of a Protected Operating System Kernel},
+    booktitle        = {IEEE Real-Time Systems Symposium},
+    address          = {Vienna, Austria}
+  }
+
+  @inproceedings{Blackham_SH_12,
+    author           = {Blackham, Bernard and Shi, Yao and Heiser, Gernot},
+    month            = apr,
+    pages            = {323-336},
+    year             = {2012},
+    title            = {Improving Interrupt Response Time in a Verifiable Protected Microkernel},
+    booktitle        = {EuroSys},
+    address          = {Bern, Switzerland}
+  }
+
 @inproceedings{Boyton_09,
   address =       {Aachen, Germany},
   author =        {Andrew Boyton},
@@ -90,6 +110,29 @@ THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT!
   doi =           {10.1145/1629575.1629596},
 }
 
+  @inproceedings{Murray_MBGBSLGK_13,
+    author           = {Murray, Toby and Matichuk, Daniel and Brassil, Matthew and Gammie, Peter and Bourke, Timothy and
+                        Seefried, Sean and Lewis, Corey and Gao, Xin and Klein, Gerwin},
+    month            = may,
+    pages            = {415-429},
+    year             = {2013},
+    title            = {{seL4}: from General Purpose to a Proof of Information Flow Enforcement},
+    booktitle        = {IEEE Symposium on Security \& Privacy},
+    address          = {San Francisco, CA}
+  }
+
+  @inproceedings{Sewell_WGMAK_11,
+    author           = {Sewell, Thomas and Winwood, Simon and Gammie, Peter and Murray, Toby and Andronick, June and Klein,
+                        Gerwin},
+    pages            = {325-340},
+    month            = aug,
+    editor           = {{Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk}},
+    year             = {2011},
+    title            = {{seL4} Enforces Integrity},
+    booktitle        = {Interactive Theorem Proving (ITP)},
+    address          = {Nijmegen, The Netherlands}
+  }
+
 @inproceedings{Tuch_KN_07,
   address =       {Nice, France},
   author =        {Harvey Tuch and Gerwin Klein and Michael Norrish},