570 lines
19 KiB
TeX
570 lines
19 KiB
TeX
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
% Copyright (c) 2015, ETH Zurich.
|
|
% All rights reserved.
|
|
%
|
|
% This file is distributed under the terms in the attached LICENSE file.
|
|
% If you do not find this file, copies can be found by writing to:
|
|
% ETH Zurich D-INFK, Universitaetstr 6, CH-8092 Zurich. Attn: Systems Group.
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
\documentclass[a4paper,11pt,twoside]{report}
|
|
\usepackage{bftn}
|
|
\usepackage{calc}
|
|
\usepackage{verbatim}
|
|
\usepackage{xspace}
|
|
\usepackage{pifont}
|
|
\usepackage{pxfonts}
|
|
\usepackage{textcomp}
|
|
\usepackage{amsmath}
|
|
\usepackage{multirow}
|
|
\usepackage{listings}
|
|
\usepackage[framemethod=default]{mdframed}
|
|
\usepackage[shortlabels]{enumitem}
|
|
\usepackage{parskip}
|
|
\usepackage{xparse}
|
|
\usepackage{ctable}
|
|
\usepackage[pdftex]{hyperref}
|
|
|
|
% hyperref setup
|
|
\definecolor{linkcol}{rgb}{0,0,0.7}
|
|
\hypersetup{
|
|
pdftitle={Barrelfish Specification},
|
|
plainpages=false,
|
|
linktocpage,
|
|
colorlinks,
|
|
linkcolor=linkcol,citecolor=linkcol,pagecolor=linkcol,urlcolor=linkcol
|
|
%breaklinks=true,pagebackref=true
|
|
}
|
|
|
|
\mdfdefinestyle{mdsyscall}{
|
|
rightline=true,
|
|
innerleftmargin=10,
|
|
innerrightmargin=10,
|
|
frametitlerulewidth=2pt,
|
|
frametitlefont={\color{white}\varname},
|
|
skipbelow=1em,
|
|
skipabove=1em,
|
|
}
|
|
|
|
\DeclareDocumentEnvironment{arguments}{}
|
|
{
|
|
\newcommand{\argument}[2]{ \item[\varname{##1}] ##2 }
|
|
\textbf{Arguments}\parskip
|
|
\begin{description}[leftmargin=!,labelwidth=\widthof{count},labelindent=1em]
|
|
}
|
|
{
|
|
\end{description}
|
|
}
|
|
|
|
\DeclareDocumentEnvironment{api}{o O {stable}}
|
|
{
|
|
\definecolor{unused}{RGB}{215,25,28}
|
|
\definecolor{unstable}{RGB}{253,174,97}
|
|
\definecolor{todo}{RGB}{255,255,191}
|
|
\definecolor{lightblue}{RGB}{171,217,233}
|
|
\definecolor{stable}{RGB}{44,123,182}
|
|
\newcommand{\brief}[1]{##1\\}
|
|
\newcommand{\note}[1]{\\\textbf{Note}\\##1\parskip}
|
|
|
|
\begin{mdframed}[style=mdsyscall,frametitle=#1,frametitlebackgroundcolor=#2]
|
|
}
|
|
{
|
|
\end{mdframed}
|
|
}
|
|
|
|
\newcommand{\fnname}[1]{\textit{\texttt{#1}}}%
|
|
\newcommand{\datatype}[1]{\textit{\texttt{#1}}}%
|
|
\newcommand{\varname}[1]{\texttt{#1}}%
|
|
\newcommand{\keywname}[1]{\textbf{\texttt{#1}}}%
|
|
\newcommand{\pathname}[1]{\texttt{#1}}%
|
|
\newcommand{\tabindent}{\hspace*{3ex}}%
|
|
\newcommand{\sockeye}{\lstinline[language=sockeye]}
|
|
\newcommand{\ccode}{\lstinline[language=C]}
|
|
|
|
% Default language for code listings is C
|
|
\lstset{
|
|
language=C,
|
|
basicstyle=\small,
|
|
frame=lines,
|
|
breaklines=true,
|
|
showstringspaces=false,
|
|
texcl=true,
|
|
columns=flexible
|
|
}
|
|
|
|
\lstdefinelanguage{Mackerel}{
|
|
morekeywords={datatype,device,register,regtype,constants,type,at,
|
|
many,edit,io,also},
|
|
sensitive=false,
|
|
morecomment=[l]{//},
|
|
morecomment=[s]{/*}{*/},
|
|
morestring=[b]",
|
|
}
|
|
|
|
% sans-serif URLs
|
|
\urlstyle{sf}
|
|
|
|
\newcommand{\todo}[1]{[\textcolor{red}{\emph{#1}}]}
|
|
|
|
\newcommand{\noarginvocation}[1]{\paragraph{#1 invocation}}
|
|
\newcounter{invocArgCnt}
|
|
\newenvironment{invocation}[1]{%
|
|
\noarginvocation{#1}
|
|
|
|
\begin{list}{\emph{Argument~\arabic{invocArgCnt}:}}{%
|
|
\usecounter{invocArgCnt}%
|
|
\setlength{\rightmargin}{\leftmargin}%
|
|
\setlength{\itemsep}{0ex}%
|
|
}
|
|
\renewcommand{\arg}{\item}
|
|
}{%
|
|
\end{list}
|
|
}
|
|
|
|
|
|
% autoref (from hyperref) setup
|
|
\def\chapterautorefname{Chapter}
|
|
\def\sectionautorefname{Section}
|
|
\def\subsectionautorefname{Section}
|
|
\expandafter\def\csname section*autorefname\endcsname{Section}
|
|
|
|
|
|
\title{Barrelfish Specification}
|
|
\author{Barrelfish project}
|
|
\tnnumber{10}
|
|
\tnkey{Specification}
|
|
|
|
\presetkeys{todonotes}{inline}{}
|
|
|
|
\begin{document}
|
|
|
|
\maketitle
|
|
|
|
\begin{versionhistory}
|
|
\vhEntry{0.1}{01.01.2009}{AB,SP,TR,AS,AK}{Initial Version}
|
|
\vhEntry{0.2}{01.01.2015}{GZ}{Update ABI etc.}
|
|
\end{versionhistory}
|
|
|
|
\cleardoublepage
|
|
\tableofcontents
|
|
|
|
\chapter{Barrelfish Kernel API}
|
|
|
|
\section{System Calls}\label{sec:syscalls}
|
|
|
|
The section defines the specification of the common system call
|
|
API that is provided by a Barrelfish CPU driver. Currently
|
|
we have the following system calls:
|
|
|
|
\begin{tabular}{|p{5cm}|>{\raggedright\arraybackslash}p{7cm}|}
|
|
\hline
|
|
|
|
SYSCALL\_INVOKE & Invoke a capability. \\
|
|
SYSCALL\_YIELD & Yield the CPU. \\
|
|
SYSCALL\_LRPC & Fast LRPC. \\
|
|
SYSCALL\_DEBUG & Benchmarking and debug syscalls. \\
|
|
SYSCALL\_REBOOT & Reboot the machine. \\
|
|
SYSCALL\_NOP & No operation. \\
|
|
SYSCALL\_PRINT & Write to console. \\
|
|
SYSCALL\_SUSPEND & Suspend the CPU. \\
|
|
SYSCALL\_GET\_ABS\_TIME & Get time elapsed since boot. \\
|
|
\hline
|
|
\end{tabular}
|
|
|
|
\subsection{SYSCALL\_INVOKE -- Capability Invocation Interface}\label{sec:sys_invoke}
|
|
|
|
The invoke call acts as a generic system call to apply operation on various OS
|
|
objects (also known as capabilities). For any given object, a distinct set of
|
|
operations are applicable depending on the capability type.
|
|
|
|
This system call takes at least one argument, which must be the address of a
|
|
capability in the caller's CSpace. The remaining arguments, if any, are
|
|
interpreted based on the type of this first capability.
|
|
|
|
Other than yielding, all kernel operations including IDC are (or should be)
|
|
provided by capability invocation, and make use of this call. The
|
|
possible invocations for every capability type are described in
|
|
the capability management document (TN-013).
|
|
|
|
This system call may only be used while the caller is
|
|
\emph{enabled}. The reason is that the caller must be prepared to
|
|
receive a reply immediately and that is only possible when
|
|
enabled, as it requires the kernel to enter the dispatcher at the
|
|
IDC entry point.
|
|
|
|
\subsection{SYSCALL\_YIELD -- Yield the CPU}\label{sec:sys_yield}
|
|
|
|
This system call yields the CPU. It takes a single argument, which must be
|
|
either the CSpace address of a dispatcher capability, or \verb CPTR_NULL .
|
|
In the first case, the given dispatcher is run unconditionally; in the
|
|
latter case, the scheduler picks which dispatcher to run.
|
|
|
|
This system call may only be used while the caller is \emph{disabled}.
|
|
Furthermore, it clears the caller's \emph{disabled} flag, so the next time
|
|
it will be entered is at the run entry point.
|
|
|
|
\subsection{SYSCALL\_DEBUG -- Debug system calls}
|
|
|
|
The debug system call (SYSCALL\_DEBUG) de-multiplexes using the second system
|
|
call argument and is defined for the following operations.
|
|
Those calls may not be supported, depending on build options,
|
|
and are not part of the regular kernel interface.
|
|
|
|
\begin{api}[DEBUG\_CONTEXT\_COUNTER\_RESET]
|
|
\brief{Sets the \varname{context\_switch\_counter} to 0.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_CONTEXT\_COUNTER\_READ]
|
|
\brief{Returns \varname{context\_switch\_counter}.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_TIMESLICE\_COUNTER\_READ]
|
|
\brief{Returns \varname{kernel\_now}.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_FLUSH\_CACHE]
|
|
\brief{Executes \fnname{wbinvd} on x86-64.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_SEND\_IPI][unstable]
|
|
\brief{Sends an interrupt to a remote core.}
|
|
\begin{arguments}
|
|
\argument{destination}{Target core.}
|
|
\argument{shorthand}{?}
|
|
\argument{vector}{IRQ number.}
|
|
\end{arguments}
|
|
\note{Is this needed with the IPI capability?}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_SET\_BREAKPOINT]
|
|
\brief{Sets a hardware breakpoint at an address.}
|
|
\begin{arguments}
|
|
\argument{addr}{Where to break.}
|
|
\argument{mode}{?}
|
|
\argument{length}{?}
|
|
\end{arguments}
|
|
\note{Use dr7 and dr0 on x86-64.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_SEND\_NOTIFY][unused]
|
|
\brief{Does only exist as a definition?}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_SLEEP][unused]
|
|
\brief{Does only exist as a definition?}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_HARDWARE\_TIMER\_READ][unstable]
|
|
\brief{Returns \fnname{tsc\_read}.}
|
|
\note{Exists only for ARM.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_HARDWARE\_TIMER\_HERTZ\_READ][unstable]
|
|
\brief{Returns \fnname{tsc\_get\_hz}.}
|
|
\note{Exists only on ARM.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_HARDWARE\_GLOBAL\_TIMER\_LOW][unstable]
|
|
\brief{Returns \fnname{gt\_read\_low}. The lower 32 bits of the timer.}
|
|
\note{Exists only in OMAP, and returns 0 on GEM 5.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_HARDWARE\_GLOBAL\_TIMER\_HIGH][unstable]
|
|
\brief{Returns global timer \fnname{gt\_read\_high}. The higher 32 bits of the timer.}
|
|
\note{Exists only in OMAP, and returns 0 on GEM 5.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_GET\_TSC\_PER\_MS][unstable]
|
|
\brief{Returns TSC (\fnname{rdtsc}) clock rate in ticks per ms.}
|
|
\note{Implemention for x86 only.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_GET\_APIC\_TIMER][unstable]
|
|
\brief{Returns the XAPIC timer counter.}
|
|
\note{Implemention for x86-64 only.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_GET\_APIC\_TICKS\_PER\_SEC][unstable]
|
|
\brief{Returns ticks per seconds of the APIC timer.}
|
|
\note{Calibrated against RTC clock. Implemention for x86-64 only.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_FEIGN\_FRAME\_CAP][unused]
|
|
\brief{Fabricates an arbitrary DevFrame cap.}
|
|
\note{Implemention for x86-32 bit only. Not used?}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_TRACE\_PMEM\_CTRL]
|
|
\brief{Enables tracing for capabilities.}
|
|
\begin{arguments}
|
|
\argument{types}{?}
|
|
\argument{start}{?}
|
|
\argument{size}{?}
|
|
\end{arguments}
|
|
\note{Implemention for x86-64 and aarch64 only.}
|
|
\end{api}
|
|
|
|
\begin{api}[DEBUG\_GET\_APIC\_ID]
|
|
\brief{Returns the xAPIC ID.}
|
|
\note{Implemention for x86-64 only.}
|
|
\end{api}
|
|
|
|
\subsection{SYSCALL\_REBOOT -- Reboot the system}
|
|
This call unconditionally hard reboots the system.
|
|
\todo{This call should be removed -AB}
|
|
|
|
\subsection{SYSCALL\_NOP}
|
|
This call takes no arguments, and returns directly to the
|
|
caller. It always succeeds.
|
|
|
|
\subsection{SYSCALL\_PRINT}
|
|
This call takes two arguments: an address in the caller's vspace, which
|
|
must be mapped, and a size, and prints the string found at that address
|
|
to the console. It may fail if any part of the string is not accessible
|
|
to the calling domain.
|
|
|
|
\subsection{SYSCALL\_SUSPEND}
|
|
\todo{should probably be a cap invocation}
|
|
|
|
\subsection{SYSCALL\_GET\_ABS\_TIME}
|
|
\todo{Figure out proper time API, they appear in various
|
|
DEBUG syscalls as well.}
|
|
|
|
|
|
\section{Dispatch and Execution}\label{sec:dispatch}
|
|
|
|
A dispatcher consists of code executing at user-level and a data
|
|
structure located in pinned memory, split into two regions. One
|
|
region is only accessible from the kernel, the other region is
|
|
shared read/write between user and kernel. The fields in the
|
|
kernel-defined part of the structure are described in
|
|
\autoref{tab:dispcb}.
|
|
|
|
\ctable[
|
|
caption=Dispatcher control structure,
|
|
label=tab:dispcb,
|
|
width=\textwidth
|
|
]{lll>{\raggedright}X}{}{
|
|
\FL
|
|
Field name & Size & Kernel R/W & Short description
|
|
\ML
|
|
\lstinline+disabled+ & word & R/W & If non-zero, the kernel will not
|
|
upcall the dispatcher, except to deliver a trap.
|
|
\NN
|
|
\lstinline+haswork+ & pointer & R & If non-zero, the kernel will
|
|
consider this dispatcher eligible to run.
|
|
\NN
|
|
\lstinline+crit_pc_low+ & pointer & R & Address of first instruction
|
|
in dispatcher's critical code section.
|
|
\NN
|
|
\lstinline+crit_pc_high+ & pointer & R & Address immediately after
|
|
last instruction of dispatcher's critical code section.
|
|
\NN
|
|
entry points & 4 function descriptors & R & Functions at which
|
|
the dispatcher code may be invoked
|
|
\NN
|
|
\lstinline+enabled_save_area+ & arch specific & W & Area for kernel
|
|
to save register state when enabled
|
|
\NN
|
|
\lstinline+disabled_save_area+ & arch specific & R/W & Area for
|
|
kernel to save and restore register state when disabled
|
|
\NN
|
|
\lstinline+trap_save_area+ & arch specific & W & Area for kernel to
|
|
save register state when a trap or a pagefault while disabled occurs
|
|
\NN
|
|
\lstinline+recv_cptr+ & capability pointer & R & Address of CNode to
|
|
store received capabilities of next local IDC into
|
|
\NN
|
|
\lstinline+recv_bits+ & word & R & Number of valid bits within
|
|
\lstinline+recv_cptr+
|
|
\NN
|
|
\lstinline+recv_slot+ & word & R & Slot within CNode to store
|
|
received capability of next local IDC into
|
|
\LL
|
|
}
|
|
|
|
Beyond these fields, the user may define and use their own data
|
|
structures (eg. a stack for the dispatcher code to execute on,
|
|
thread management structures, etc).
|
|
|
|
\subsection{Disabled}
|
|
|
|
A dispatcher is considered disabled by the kernel if either of the
|
|
following conditions is true:
|
|
|
|
\begin{itemize}
|
|
\item its disabled word is non-zero
|
|
\item its program counter is within the range specified by the
|
|
\lstinline+crit_pc_low+ and \lstinline+crit_pc_high+ fields
|
|
\end{itemize}
|
|
|
|
The disabled state of a dispatcher controls where the kernel saves
|
|
its registers, and is described in the following subsection. When
|
|
the kernel resumes a dispatcher that was last running while
|
|
disabled, it restores its machine state and resumes execution at the
|
|
saved instruction, rather than upcalling it at an entry point.
|
|
|
|
\subsection{Register save areas}
|
|
|
|
The dispatcher structure contains enough space for three full copies
|
|
of the machine register state to be saved. The \lstinline+trap_save_area+
|
|
is used whenever the dispatcher takes a trap, regardless of whether
|
|
it is enabled or disabled. Otherwise, the \lstinline+disabled_save_area+
|
|
is used whenever the dispatcher is disabled (see above), and the
|
|
\lstinline+enabled_save_area+ is used in all other cases.
|
|
|
|
\autoref{fig:dispstatesaves} (Trap and PageFault states have
|
|
been left out for brevity) shows important dispatcher states and into
|
|
which register save area state is saved upon a state transition. The
|
|
starting state for a domain is ``notrunning'' and depicted with a
|
|
bold border in the Figure.
|
|
|
|
\begin{figure}
|
|
\centering
|
|
\includegraphics[width=\textwidth]{disp_states_simple_save_area_analysis}
|
|
\caption[Dispatcher state save areas]{Dispatcher state save areas.
|
|
Trap and PageFault states
|
|
omitted for brevity. Regular text and lines denote state changes
|
|
by the kernel. Dashed lines and italic text denote state changes
|
|
by user-space, which do not necessarily have to use the denoted
|
|
save area. The starting state is in the bold
|
|
node.}\label{fig:dispstatesaves}
|
|
\end{figure}
|
|
|
|
Arrows from right to left involve saving state into the labeled
|
|
area. Arrows from left to right involve restoring state from the
|
|
labeled area. It can be seen that no state can be overwritten. The
|
|
kernel can recognize a disabled dispatcher by looking at the
|
|
disabled flag, as well as the domain's instruction pointer. Nothing
|
|
else needs to be examined.
|
|
|
|
The dispatcher states are also depicted in \autoref{fig:dispstates}.
|
|
|
|
\subsection{Dispatcher Entry Points}
|
|
|
|
Unless restoring it from a disabled context, the kernel always
|
|
enters a dispatcher at one of the following entry
|
|
points. Whenever the kernel invokes a dispatcher at any of its entry
|
|
points, it sets the disabled bit on. One (ABI-specific) register
|
|
always points to the dispatcher structure. The value of all other
|
|
registers depends on the entry point at which the dispatcher is
|
|
invoked, and is described below.
|
|
|
|
The entry points are:
|
|
|
|
\begin{description}
|
|
\item[Run] A dispatcher is entered at this entry point when it was
|
|
not previously running, the last time it ran it was either enabled or
|
|
yielded the CPU, and the kernel has given it the CPU. Other than the
|
|
register that holds a pointer to the dispatcher itself, all other registers
|
|
are undefined. The dispatcher's last machine state is saved in the
|
|
\lstinline+enabled_save_area+.
|
|
|
|
\item[PageFault] A dispatcher is entered at this entry point when it
|
|
suffers a page fault while enabled. On entry, the dispatcher register is
|
|
set, and the argument registers contain information about the cause of
|
|
the fault. Volatile registers are saved in the
|
|
\lstinline+enabled_save_area+; all other registers contain the user
|
|
state at the time of the fault.
|
|
|
|
\item[PageFault\_Disabled] A dispatcher is entered at this entry point when it
|
|
suffers a page fault while disabled. On entry, the dispatcher register is
|
|
set, and the argument registers contain information about the cause of
|
|
the fault. Volatile registers are saved in the
|
|
\lstinline+trap_save_area+; all other registers contain the user
|
|
state at the time of the fault.
|
|
|
|
\item[Trap] A dispatcher is entered at this entry point when it is
|
|
running and it raises an exception (for example, illegal
|
|
instruction, divide by zero, breakpoint, etc.). Unlike the other
|
|
entry points, a dispatcher may be entered at its trap entry even
|
|
when it was running disabled. The machine state at the time of the
|
|
trap is saved in the \lstinline+trap_save_area+, and the argument
|
|
registers convey information about the cause of the trap.
|
|
|
|
\item[LRPC] A dispatcher is entered at this entry point when an
|
|
LRPC message (see below) is delivered to it. This can only
|
|
happen when it was not previously running, and was enabled. On
|
|
entry, four registers are delivered containing the message payload,
|
|
one stores the endpoint offset, and another contains the dispatcher pointer.
|
|
\end{description}
|
|
|
|
This diagram shows the states a \emph{dispatcher} can be in and how it
|
|
gets there. The exceptional states Trap and PageFault have been
|
|
omitted for brevity.
|
|
|
|
\begin{figure}
|
|
\centering
|
|
\includegraphics[width=.7\columnwidth]{disp_states_simple}
|
|
\caption[Typical dispatcher states]{Typical dispatcher states.
|
|
Trap and PageFault states
|
|
omitted for brevity. Regular text and lines denote state changes
|
|
by the kernel. Dashed lines and italic text denote state changes
|
|
by user-space. The starting state is in bold.}
|
|
\label{fig:dispstates}
|
|
\end{figure}
|
|
|
|
\subsection{Interrupt delivery}\label{sec:interrupts}
|
|
|
|
Hardware interrupts are delivered by the kernel as asynchronous IDC
|
|
messages to a registered dispatcher. A dispatcher can be registered
|
|
as for a specific IRQ by invoking the IRQTable capability,
|
|
passing it an IDC endpoint to the dispatcher and the IRQ
|
|
number. It is not possible for multiple IDC endpoints to be
|
|
registered with the same IRQ number at any one time.
|
|
|
|
Henceforth, the kernel will send an IDC message using asynchronous
|
|
delivery to the registered endpoint. Asynchronous
|
|
IDC is used as it does not cause priority inversion by directly
|
|
dispatching the target dispatcher.
|
|
|
|
\subsection{Exception delivery}
|
|
|
|
When a CPU exception happens in user-space, it is reflected to the
|
|
dispatcher on which it appeared. Page
|
|
faults are dispatched to the page-fault entry point of the
|
|
dispatcher. All other exceptions are dispatched to the trap entry
|
|
point of the dispatcher. The disabled flag of the dispatcher is
|
|
ignored in all cases and state is saved to the trap save area.
|
|
|
|
\section{Scheduling}
|
|
|
|
Upon reception of a timer interrupt, the kernel calls `schedule()`,
|
|
which selects the next dispatcher to run. At the moment, a simple
|
|
round-robin scheduler is implemented that walks a circular
|
|
singly-linked list forever.
|
|
\todo{RBED, gang-scheduling}
|
|
|
|
\section{TODO}
|
|
\begin{itemize}
|
|
\item virtual machine support
|
|
\item timers
|
|
\item resource management
|
|
\item thread migration
|
|
\item event tracing / performance monitoring
|
|
\end{itemize}
|
|
|
|
\chapter{Barrelfish Library API}
|
|
\todo{Documentation of libbarrelfish}
|
|
|
|
\subsection{Initial Capability Space}
|
|
|
|
The initial capability space of other domains is similar, but lacks the other
|
|
cnodes in the root cnode, as illustrated in \autoref{fig:app_cspace}.
|
|
|
|
\begin{figure}
|
|
\centering
|
|
\includegraphics[width=\textwidth]{app_cspace}
|
|
\caption{initial capability space layout of user tasks}
|
|
\label{fig:app_cspace}
|
|
\end{figure}
|
|
|
|
|
|
\chapter*{Acknowledgements}
|
|
Paul, Rebecca, Tim, et al.
|
|
|
|
|
|
\bibliographystyle{plain}
|
|
\bibliography{defs,barrelfish}
|
|
\end{document}
|