1331722Seadler% 218316Swollman% Copyright 2014, General Dynamics C4 Systems 318316Swollman% 418316Swollman% SPDX-License-Identifier: GPL-2.0-only 518316Swollman% 618316Swollman 718316Swollman\chapter{\label{ch:bootup}System Bootstrapping} 818316Swollman 918316Swollman\section{Initial Thread's Environment} 1018316Swollman 1118316SwollmanThe seL4 kernel creates a minimal boot environment for the initial thread, which 1218316Swollman is started at priority \texttt{seL4\_MaxPrio} and maximum control priority \texttt{seL4\_MaxPrio}. 1318316SwollmanThis environment consists of the initial thread's TCB, CSpace and VSpace, 1418316Swollmanconsisting of frames that contain the userland image (code/data of the initial 1518316Swollmanthread) and the IPC buffer. 1618316Swollman 1718316SwollmanOn the MCS kernel, the initial thread is configured with a round-robin scheduling context 1818316Swollmanwith \texttt{CONFIG\_BOOT\_THREAD\_TIME\_SLICE} milliseconds timeslice. 1918316SwollmanWithout MCS, all threads including the initial thread are scheduled round-robin with 2018316Swollman\texttt{CONFIG\_TIMER\_TICK\_MS} $*$ \texttt{CONFIG\_TIME\_SLICE} timeslices. 2118316Swollman 2218316SwollmanThe initial thread's CSpace consists of exactly one CNode 2318316Swollmanwhich contains capabilities to the initial 2418316Swollmanthread's own resources as well as to all available global resources. 2518316SwollmanThe CNode size can be configured at compile time (default is $2^{12}$ 2618316Swollmanslots), but the guard is always chosen so that the CNode resolves exactly 2718316Swollmanthe number of bits in the architecture (32 bits or 64 bits). This means, the 2818316Swollmanfirst slot of the CNode has CPTR 0x0, the second slot has CPTR 0x1 etc. 2946303Smarkm 3046303SmarkmThe first 12 slots contain specific capabilities as listed in 3150476Speter\autoref{tab:cnode_content}. 3218316Swollman 3318316Swollman\begin{table}[htb] 3418316Swollman \begin{center} 3518316Swollman \caption{Initial thread's CNode content.} 3618316Swollman \label{tab:cnode_content} 3718316Swollman \begin{tabularx}{\textwidth}{lX} 3818316Swollman \toprule 3918316Swollman Enum Constant & Capability \\ 40126250Sbms \midrule 4146303Smarkm \texttt{seL4\_CapNull} & null \\ 42126250Sbms \texttt{seL4\_CapInitThreadTCB} & initial thread's TCB \\ 43126250Sbms \texttt{seL4\_CapInitThreadCNode} & initial thread's CNode \\ 44126250Sbms \texttt{seL4\_CapInitThreadVSpace} & initial thread's VSpace \\ 45126250Sbms \texttt{seL4\_CapIRQControl} & global IRQ controller (see \autoref{sec:interrupts}) \\ 46126250Sbms \texttt{seL4\_CapASIDControl} & global ASID controller (see \autoref{ch:vspace}) \\ 4746303Smarkm \texttt{seL4\_CapInitThreadASIDPool} & initial thread's ASID pool (see \autoref{ch:vspace}) \\ 4846303Smarkm \texttt{seL4\_CapIOPort} & global I/O port cap, null cap if unsupported 4918316Swollman\ifxeightsix 5018316Swollman(see \autoref{sec:ioports}) 5118316Swollman\fi 5218316Swollman\\ 5318316Swollman \texttt{seL4\_CapIOSpace} & global I/O space cap, null cap if unsupported 54190715Sphk\ifxeightsix 55190715Sphk(see \autoref{sec:iospace}) 5618316Swollman\fi 57190718Sphk\\ 58190715Sphk \texttt{seL4\_CapBootInfoFrame} & BootInfo frame (see \autoref{ch:bootup:bootinfo}) \\ 5918316Swollman \texttt{seL4\_CapInitThreadIPCBuffer} & initial thread's IPC buffer (see \autoref{sec:messageinfo}) \\ 6018316Swollman \texttt{seL4\_CapDomain} & domain cap (see \autoref{sec:domains}) \\ 6118316Swollman \texttt{seL4\_CapInitThreadSC} & initial thread's scheduling context (MCS only) \\ 6246303Smarkm \bottomrule 6346303Smarkm \end{tabularx} 6418316Swollman \end{center} 6546303Smarkm\end{table} 66190715Sphk 67190715Sphk\section{\label{ch:bootup:bootinfo}BootInfo Frame} 68190715Sphk 69190715SphkCNode slots with CPTR \texttt{seL4\_NumInitialCaps} (defined in the seL4 7018316Swollmanuserland library) and above are filled dynamically during 7118316Swollmanbootstrapping. Their exact contents depend on the userland image size, 7218316Swollmanplatform configuration (devices) etc. In order to tell the initial thread 7318316Swollmanwhich capabilities are stored where in its CNode, the kernel provides 7418316Swollmana \emph{BootInfo Frame} which is mapped into the initial thread's address 7518316Swollmanspace. The mapped address is chosen by the kernel and given to the initial 7618316Swollmanthread via a CPU register. 7718316Swollman 7818316SwollmanThe BootInfo Frame contains the C struct described in 7918316Swollman\autoref{tab:bootinfo_struct}. 8018316SwollmanIt is defined in the seL4 userland library. Besides talking about 8118316Swollmancapabilities, it also informs the initial thread about 8218316Swollmanthe current platform's configuration. 8318316Swollman 8418316SwollmanThe type \texttt{seL4\_SlotRegion} is a C struct 8518316Swollmanwhich contains \texttt{start} and \texttt{end} slot CPTRs. It denotes a region 8618316Swollmanof slots in the initial thread's CNode, starting with CPTR \texttt{start} and with 8718316Swollman\texttt{end} being the CPTR of the first slot after the region ends, i.e.\ 8818316Swollman\texttt{end - 1} points to the last slot of the region. 8918316Swollman 9018316Swollman\begin{table}[htb] 9118316Swollman \begin{center} 9218316Swollman \caption{BootInfo struct.} 9318316Swollman \label{tab:bootinfo_struct} 9418316Swollman \begin{tabularx}{\textwidth}{llX} 9518316Swollman \toprule 9618316Swollman Field Type & Field Name & Description \\ 9718316Swollman \midrule 9818316Swollman \texttt{seL4\_Word} & \texttt{extraLen} & length of additional bootinfo information in bytes \\ 9918316Swollman \texttt{seL4\_NodeId} & \texttt{nodeID} & node ID \\ 100229778Suqs \texttt{seL4\_Word} & \texttt{numNodes} & number of nodes \\ 10118316Swollman \texttt{seL4\_Word} & \texttt{numIOPTLevels} & number of I/O page-table levels (-1 if CONFIG\_IOMMU unset) \\ 10218316Swollman \texttt{seL4\_IPCBuffer*} & \texttt{ipcBuffer} & pointer to the initial thread's IPC buffer \\ 10318316Swollman \texttt{seL4\_SlotRegion} & \texttt{empty} & empty slots (null caps) \\ 10418316Swollman \texttt{seL4\_SlotRegion} & \texttt{sharedFrames} & reserved \\ 105190715Sphk \texttt{seL4\_SlotRegion} & \texttt{userImageFrames} & frames containing the userland image \\ 10618316Swollman \texttt{seL4\_SlotRegion} & \texttt{userImagePaging} & userland-image paging structure caps \\ 10718316Swollman \texttt{seL4\_SlotRegion} & \texttt{ioSpaceCaps} & I/O space capabilities for ARM SMMU \\ 10818316Swollman \texttt{seL4\_SlotRegion} & \texttt{extraBIPages} & frames backing additional bootinfo information \\ 10946303Smarkm \texttt{seL4\_Uint8} & \texttt{initThreadCNodeSizeBits} & CNode size ($2^n$ slots) \\ 11046303Smarkm \texttt{seL4\_Word} & \texttt{initThreadDomain} & domain of the initial thread (see \autoref{sec:domains}) \\ 11118316Swollman \texttt{seL4\_SlotRegion} & \texttt{schedcontrol} & seL4\_SchedControl capabilities, one for each node (MCS only). \\ 11218316Swollman \texttt{seL4\_SlotRegion} & \texttt{untyped} & untyped-memory capabilities \\ 11318316Swollman \texttt{seL4\_UntypedDesc[]} & \texttt{untypedList} & array of information about each untyped \\ 11418316Swollman \bottomrule 11518316Swollman \end{tabularx} 11618316Swollman \end{center} 11718316Swollman\end{table} 11818316Swollman 11918316SwollmanDepending on the architecture and platform there might be additional pieces of boot 12018316Swollmaninformation. If \texttt{extraLen} is greater then zero then 4K after the start of bootinfo 121190715Sphkis a region of extraLen bytes containing additional bootinfo structures. Each chunk starts 12218316Swollmanwith a \texttt{seL4\_BootInfoHeader}, described in \autoref{tab:bi_header_struct}, that 12318316Swollmandescribes what the chunk is and how long it is, where the length includes the header. The 12418316Swollmanlength can be used to skip over chunks that you do not understand. The only generally 12518316Swollmandefined chunk type is \texttt{SEL4\_BOOTINFO\_HEADER\_PADDING} and describes an empty 12646303Smarkmchunk that has no data, any other types are platform or architecture specific. The 12746303Smarkm\texttt{extraBIPages} slot region gives the frames capabilities for the pages that make up 12818316Swollmanthe additional boot info region. 12918316Swollman 13018316Swollman\begin{table}[htb] 13118316Swollman \begin{center} 13218316Swollman \caption{BootInfoHeader struct.} 13318316Swollman \label{tab:bi_header_struct} 13418316Swollman \begin{tabular}{lll} 13518316Swollman \toprule 13618316Swollman Field Type & Field Name & Description \\ 13718316Swollman \midrule 13818316Swollman \texttt{seL4\_Word} & \texttt{id} & Identifier indicating the contents of the chunk \\ 139190715Sphk \texttt{seL4\_Uint8} & \texttt{len} & Length in bytes of the chunk \\ 14018316Swollman \bottomrule 14118316Swollman \end{tabular} 14246303Smarkm \end{center} 14346303Smarkm\end{table} 14418316Swollman 14518316SwollmanThe capabilities in \texttt{userImageFrames} are 14618316Swollmanordered such that the first capability references the first frame of the 14718316Swollmanuserland image and so on. 14818316SwollmanThe capabilities in \texttt{userImagePaging} are ordered in descending order 14918316Swollmanof paging structure size. Within a given paging structure size, capabilities are 15018316Swollmanordered by the virtual address at which the corresponding objects are mapped 15118316Swollmaninto the initial thread's address space. 15218316Swollman 15318316SwollmanIt is up to userland to infer the virtual address of frames referenced by 15418316Swollmanthe capabilities in \texttt{userImageFrames} and the virtual address and 15518316Swollmantypes of paging structures 15618316Swollmanreferenced by the capabilities in \texttt{userImagePaging}. 15718316SwollmanUserland typically has a way of finding out to which virtual addresses its 15818316Swollmancode and data is mapped (e.g.\ in GCC, with the standard linker script, the 15918316Swollmansymbols \texttt{\_\_executable\_start} and \texttt{\_end} are available). 16018316SwollmanAdditionally, the initial thread can assume that its address space is virtually 16118316Swollmancontiguous, and is made up of the smallest frames available on the architecture. 16218316SwollmanIt's also assumed that the initial thread knows which paging structures are 16318316Swollmanavailable on the architecture it's running on. 16418316SwollmanThis, along with knowledge of how capabilities in \texttt{userImageFrames} and 165190715Sphk\texttt{userImagePaging} are ordered, is sufficient information for userland to infer 16646303Smarkmthe virtual address of each 16718316Swollmanframe capability, and the virtual address and type of each paging structure capability. 16846303Smarkm 16918316SwollmanUntyped memory is given in no particular order. The array entry 17018316Swollman\texttt{untypedList[i]} stores the untyped-memory information of 17118316Swollmanthe i-th untyped cap of the slot region \texttt{untyped}. Therefore, the array 172299768Spfglength is at least \texttt{untyped.end - untyped.start}. The actual length is 173299768Spfghardcoded in the kernel and irrelevant to the reader of the array. The untyped 17418316Swollmanmemory information is stored in a \texttt{seL4\_UntypedDesc} struct, described 17518316Swollmanin \autoref{tab:untyped_desc_struct}, and details the address, size and kind of 17618316Swollmanthe memory backing the untyped. This allows userland to infer physical memory 17718316Swollmanaddresses of retyped frames and use them to initiate DMA transfers when no 17818316SwollmanIOMMU is available. The kernel makes no guarantees about certain sizes of untyped 17918316Swollmanmemory being available. 18018316Swollman 18118316Swollman\begin{table}[htb] 18218316Swollman \begin{center} 18318316Swollman \caption{seL4\_UntypedDesc struct} 18418316Swollman \label{tab:untyped_desc_struct} 18518316Swollman \begin{tabular}{lll} 18646303Smarkm \toprule 18746303Smarkm Field Type & Field Name & Description \\ 18818316Swollman \midrule 18918316Swollman \texttt{seL4\_Word} & \texttt{paddr} & physical base address of the untyped object \\ 19046303Smarkm \texttt{seL4\_Uint8} & \texttt{sizeBits} & size ($2^n$ bytes) of the untyped object \\ 19118316Swollman \texttt{seL4\_Uint8} & \texttt{isDevice} & is this untyped a device or not (see \autoref{sec:kernmemalloc}) \\ 19218316Swollman \texttt{seL4\_Uint8[]} & \texttt{padding} & manual padding so final struct is a multiple of the word size \\ 19318316Swollman \bottomrule 194299768Spfg \end{tabular} 19518316Swollman \end{center} 19618316Swollman\end{table} 19718316Swollman 19818316SwollmanIf the platform has an seL4-supported IOMMU, \texttt{numIOPTLevels} contains 19918316Swollmanthe number of IOMMU-page-table levels. This information is needed by userland 20018316Swollmanwhen constructing an IOMMU address space (IOSpace). If there is no IOMMU 20118316Swollmansupport, \texttt{numIOPTLevels} is \texttt{0}. 20218316Swollman 20318316SwollmanOn ARM if the platform has any available SMMU units the capabilities for them 20418316Swollmanwill be described by the \texttt{ioSpaceCaps} slot region. The mapping of a 205190715Sphkcapability from this region to a specific SMMU is platform specific. 20618316Swollman 20718316Swollman\ifxeightsix 20818316Swollman\section{Boot Command-line Arguments} 20918316Swollman 21046303SmarkmOn IA-32, seL4 accepts boot command-line arguments which are passed to the 21146303Smarkmkernel via a multiboot-compliant bootloader (e.g.\ GRUB, syslinux). Multiple 21218316Swollmanarguments are separated from each other by whitespace. Two forms of arguments 21318316Swollmanare accepted: 21418316Swollman(1) key-value arguments of the form ``key=value'' and (2) single keys of the 21546303Smarkmform ``key''. The value field of the key-value form may be a string, a decimal 21618316Swollmaninteger, a hexadecimal integer beginning with ``0x'', or an integer list where 21718316Swollmanlist elements are separated by commas. 21818316SwollmanKeys and values can't have any whitespace in them and there can be no 21918316Swollmanwhitespace before or after an ``='' or a comma either. 22018316SwollmanArguments are listed in \autoref{tab:bootargs} along with their default values (if left unspecified). 22118316Swollman 22218316Swollman 22318316Swollman\begin{table}[htb] 22418316Swollman \caption{IA-32 boot command-line arguments.} 22518316Swollman \begin{tabularx}{\textwidth}{lXX} 22618316Swollman \toprule 22718316Swollman Key & Value & Default \\ 22818316Swollman \midrule 22918316Swollman \texttt{console\_port} & 23018316Swollman I/O-port base of the serial port that the kernel prints to 23118316Swollman (if compiled in debug mode) & 23218316Swollman 0x3f8 \\ 23318316Swollman \texttt{debug\_port} & 23418316Swollman I/O-port base of the serial port that is used for kernel debugging 23518316Swollman (if compiled in debug mode) & 23618316Swollman 0x3f8 \\ 23718316Swollman \texttt{disable\_iommu} & 23818316Swollman none & 23918316Swollman The IOMMU is enabled by default on VT-d-capable platforms \\ 24018316Swollman \bottomrule 24118316Swollman \end{tabularx} 24218316Swollman \label{tab:bootargs} 24318316Swollman\end{table} 24418316Swollman\fi 24518316Swollman