seL4/haskell/doc/refman.tex

%
% Copyright 2014, General Dynamics C4 Systems
%
% This software may be distributed and modified according to the terms of
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
% See "LICENSE_GPLv2.txt" for details.
%
% @TAG(GD_GPL)
%

\documentclass[a4paper,11pt,twoside]{report}
\usepackage[colour,nictaonly]{disy}

\usepackage{comment}
\usepackage{ifxetex,ifpdf}
\usepackage{alltt}
\usepackage[T1]{fontenc}

\usepackage[margin=33mm]{geometry}
\usepackage{cite,fancyhdr,microtype,tocloft}

\pagestyle{fancyplain}
\lhead[\fancyplain{}{\sl\thepage}]{\fancyplain{}{\sl\rightmark}}
\chead{}
\rhead[\fancyplain{}{\sl\leftmark}]{\fancyplain{}{\sl\thepage}}
\lfoot[\fancyplain{\sl\thepage}{}]{}
\cfoot{}
\rfoot[]{\fancyplain{\sl\thepage}{}}

\definecolor{linkcolor}{rgb}{0,0,0.4}
\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,
            filecolor=linkcolor,urlcolor=linkcolor]{hyperref}

\setlength{\cftsubsecnumwidth}{4em}
\setlength{\cftsecnumwidth}{6ex}

\newcommand{\softwareversion}{\input{version.txt}}

% Definitions of the appearance of the typeset Haskell code
\ifxetex
\usepackage{fontspec}
\defaultfontfeatures{Scale=MatchLowerCase,Mapping=tex-text}
%\newfontfamily\hsfamily[Scale=0.85,BoldFont={Latin Modern Mono}, SmallCapsFont={Latin Modern Mono Caps}]{Latin Modern Mono Light}
\newfontfamily\hsfamily[Scale=0.91,SmallCapsFont={Fontin Sans Small Caps}]{Fontin Sans}
\else
%\newcommand{\hsfamily}{\ttfamily}
\newcommand{\hsfamily}{\sffamily}
\fi

% Command used to mark Haskell-specific implementation details so we can easily remove them from the manual
%\includecomment{impdetails}
\excludecomment{impdetails}
%\newif \ifimpdetails \impdetailstrue
%\newenvironment{impdetails}{
% \ifimpdetails\begin{comment}\fi}{\ifimpdetails\end{comment}\fi}

\usepackage{lambdaTeX}

% Workaround for conflict between PDFTeX and lambdaTeX
\catcode`\<=12
\catcode`\>=12

% XXX work around broken tex-text mapping
\ifxetex\typeset{`}{\hbox{\hsfamily\addfontfeatures{Mapping=none} `}}\fi

% Symbols for bitwise AND and OR
\typeset{.|.}{$\ddot{\vee}$}
\typeset{.&.}{$\ddot{\wedge}$}

% Symbols for monad bind operators
\typeset{>>}{$\gg$}
\typeset{<<}{$\ll$}
\typeset{>>=}{$\gg\joinrel\joinrel\Relbar$}
\typeset{=<<}{$\Relbar\joinrel\joinrel\ll$}

\typeout{If TeX stops here, run mkfunctions.pl to generate functions.aux}
\input{functions.aux}

\hyphenation{C-Space C-Spaces C-Node C-Nodes Has-kell Send-Wait Ex-change-Reg-ist-ers Thread-Con-trol}

\begin{document}

\title{seL4 Haskell Manual}
\author{Trustworthy~Systems~Team, NICTA}
\AuthorEmail{ssrg@nicta.com.au}
\date{\softwareversion}

\maketitle

  \urlstyle{sf}
  \thispagestyle{empty}

  \vfill

  \copyright\ General Dynamics C4 Systems.\\

  \textsc{All rights reserved}.

  % Acknowledgements
  \thispagestyle{empty}
  \vfill
  \renewcommand{\abstractname}{Acknowledgements}
  \begin{abstract}
The seL4 project team would like to acknowledge the following people
and teams (in no particular order) who have contributed to seL4 in
some way. Apologies if we missed you.

seL4 is a descendant of L4 itself, and thus owes a lot to Jochen
Liedtke's work on microkernels.

The L4Ka team at the University of Karlsruhe and Hermann H\"{a}rtig's
operating system group at TU Dresden have provided many fruitful
discussions that have influenced seL4's design.

Jonathon Shapiro has also provided insightful interaction on many
occasions, and his work on EROS and its successor Coyotos has also
influenced seL4's design.

We would also like to thank Gerwin Klein and his L4.verified
project team at NICTA for their insights and continual feedback on
our work. David Cock deserves special mention for his work on
bringing the ARM simulator into being.

\vspace{5ex}
\begin{center}
{\large\textbf{Warning}}
\end{center}
This manual is currently out of date. While the Haskell code itself is kept
up-to-date, the text in this manual describes an old version of seL4 and uses
outdated/deprecated terminology.
\begin{center}
Use with caution.
\end{center}
\end{abstract}

  \thispagestyle{empty}

  \cleardoublepage
  \setcounter{page}{1}
  \tableofcontents

  \cleardoublepage
  \setcounter{page}{1}
  \pagenumbering{arabic}
  
% Re-enable lambdaTeX's active < and >
\catcode`\<=\active
\catcode`\>=\active


\part{Introduction}

\chapter{Introduction}

This manual documents the seL4 kernel reference implementation, which
is written in Haskell. It provides annotated Haskell source code
describing the high-level, architecture independent behaviour of the
three services that the kernel provides --- threads, address spaces,
and communication --- including the system calls used to control them
from user level. This source code is executable --- not pseudocode ---
and forms part of a simulator which can be used to examine the
behaviour of a running seL4 kernel.

\autoref{sec:overview} provides an overview of the seL4 API. \autoref{sec:haskell} briefly discusses Haskell, and the manner in which we have applied it to construct the reference implementation. The remaining chapters are generated directly from the Haskell source code of the reference implementation, and contain all of the code (apart from some Haskell-specific implementation details, such as compiler and pre-processor directives).

\chapter{seL4 Overview}\label{sec:overview}
\input{overview.tex}

\chapter{Haskell Model Overview}\label{sec:haskell}
\input{haskell.tex}

\part{Annotated Source Code}

\chapter{Kernel API}\label{sec:api}

This chapter documents the parts of the kernel that interact directly with user-level code.

\section{Kernel Object Types}\label{sec:api.types}
\input{../src/SEL4/API/Types.lhs}

\section{Machine-Independent Object Types}\label{sec:api.types.universal}
\input{../src/SEL4/API/Types/Universal.lhs}

\section{Kernel Object Invocations}\label{sec:api.invocation}
\input{../src/SEL4/API/Invocation.lhs}

\section{System Calls}\label{sec:api.syscall}
\input{../src/SEL4/API/Syscall.lhs}

\section{System Call Failures}\label{sec:api.failures}
\input{../src/SEL4/API/Failures.lhs}

\section{Faults and Exceptions}\label{sec:api.faults}
\input{../src/SEL4/API/Faults.lhs}

\chapter{Kernel Operations}\label{sec:kernel}

This chapter documents operations within the kernel that are not directly related to a single kernel object.

\section{Capability Space Lookups}\label{sec:kernel.cspace}
\input{../src/SEL4/Kernel/CSpace.lhs}

\section{Threads and Scheduling}\label{sec:kernel.thread}
\input{../src/SEL4/Kernel/Thread.lhs}

\section{Bootstrapping the Kernel}\label{sec:kernel.init}
\input{../src/SEL4/Kernel/Init.lhs}

\section{Handling Faults}\label{sec:kernel.faulthandler}
\input{../src/SEL4/Kernel/FaultHandler.lhs}

\section{Virtual Memory}\label{sec:kernel.vspace}
\input{../src/SEL4/Kernel/VSpace.lhs}

\chapter{Kernel Objects}\label{sec:object}

This chapter defines the first-class kernel objects, including their representation in physical memory, and the operations that may be performed on them by user-level threads and by other kernel-level code.

\section{Data Structures}\label{sec:object.structures}
\input{../src/SEL4/Object/Structures.lhs}

\section{Thread Control Blocks}\label{sec:object.tcb}
\input{../src/SEL4/Object/TCB.lhs}

\section{Capability Nodes}\label{sec:object.cnode}
\input{../src/SEL4/Object/CNode.lhs}

\section{Synchronous Endpoints}\label{sec:object.endpoint}
\input{../src/SEL4/Object/Endpoint.lhs}

\section{Asynchronous Endpoints}\label{sec:object.asyncendpoint}
\input{../src/SEL4/Object/AsyncEndpoint.lhs}

\section{Untyped Objects}\label{sec:object.untyped}
\input{../src/SEL4/Object/Untyped.lhs}

\section{Interrupt Controller and Handler Objects}\label{sec:object.interrupt}
\input{../src/SEL4/Object/Interrupt.lhs}

\section{Type-Specific Operations}\label{sec:object.objecttype}
\input{../src/SEL4/Object/ObjectType.lhs}

\section{Storing Objects}\label{sec:object.instances}
\input{../src/SEL4/Object/Instances.lhs}

\chapter{Haskell Model Details}\label{sec:model}

This chapter describes implementation details of the Haskell kernel. It should not be necessary to read this section to understand the API; however, it may help in understanding the way the model works.

\section{System State}\label{sec:model.statedata}
\input{../src/SEL4/Model/StateData.lhs}

\section{Physical Address Space Model}\label{sec:model.pspace}
\input{../src/SEL4/Model/PSpace.lhs}

\section{System Calls}\label{sec:model.syscall}
\input{../src/SEL4/Model/Syscall.lhs}

\section{Failures}\label{sec:model.failures}
\input{../src/SEL4/Model/Failures.lhs}

\section{Preemption}\label{sec:model.preemption}
\input{../src/SEL4/Model/Preemption.lhs}

\chapter{Modelling the Hardware}\label{sec:machine}\label{ch:code:machine}

This chapter defines the interface that is used by the rest of the kernel to represent the underlying hardware.

\section{Words and Registers}\label{sec:machine.registerset}
\input{../src/SEL4/Machine/RegisterSet.lhs}

\section{Hardware Functions}\label{sec:machine.hardware}
\input{../src/SEL4/Machine/Hardware.lhs}

\part{Architecture-Specific Features}

\chapter{Generic Implementations}

This chapter contains default definitions for platforms with no special requirements.

\section{Capability-based Virtual Address Space}
\input{../src/SEL4/Kernel/VSpace/CSpace.lhs}

\chapter{ARM}

This chapter defines the implementation-specific parts of the API for the ARM architecture. The ARM support is designed for version 6 or later of the ARM architecture. In particular, it uses the ARMv6 page table format, and does not make use of the Fast Context Switch Extension which is performance-critical on ARMv5 and earlier.

\section{Register Set}
\input{../src/SEL4/Machine/RegisterSet/ARM.lhs}

\section{Hardware Interface}
\input{../src/SEL4/Machine/Hardware/ARM.lhs}

\section{Kernel Object Types}
\input{../src/SEL4/API/Types/ARM.lhs}

\section{Kernel Object Invocations}
\input{../src/SEL4/API/Invocation/ARM.lhs}

\section{Kernel Object Data}
\input{../src/SEL4/Object/Structures/ARM.lhs}

\section{Type-Specific Operations}
\input{../src/SEL4/Object/ObjectType/ARM.lhs}

\section{Storing Objects}
\input{../src/SEL4/Object/Instances/ARM.lhs}

\section{Global Kernel Data}
\input{../src/SEL4/Model/StateData/ARM.lhs}

\section{Interrupt Handling}
\input{../src/SEL4/Object/Interrupt/ARM.lhs}

\section{Virtual Address Space}
\input{../src/SEL4/Kernel/VSpace/ARM.lhs}

\section{Switching Threads}
\input{../src/SEL4/Kernel/Thread/ARM.lhs}

\section{Copying Coprocessor Registers}
\input{../src/SEL4/Object/TCB/ARM.lhs}

\begin{impdetails}

\chapter{Simple Haskell-based Simulator}

This chapter defines a language and interpreter that may be used for writing simple test programs for the seL4 API. The language is intended to look similar to the assembly language of a simple RISC processor. This chapter also defines implementation-specific API features for the simulated machine.

\section{Register Set}
\input{../src/SEL4/Machine/RegisterSet/HaskellCPU.lhs}

\section{Hardware Interface}
\input{../src/SEL4/Machine/Hardware/HaskellCPU.lhs}

\section{API}
\input{../src/SEL4/API/Types/HaskellCPU.lhs}

\section{Kernel Objects}
\input{../src/SEL4/Object/ObjectType/HaskellCPU.lhs}

\section{Virtual Address Space}
\input{../src/SEL4/Kernel/VSpace/HaskellCPU.lhs}

\end{impdetails}

\bibliographystyle{plain}
\bibliography{pubs}

\end{document}