1% 2% Copyright 2014, General Dynamics C4 Systems 3% 4% SPDX-License-Identifier: GPL-2.0-only 5% 6 7\chapter{\label{ch:bootup}System Bootstrapping} 8 9\section{Initial Thread's Environment} 10 11The seL4 kernel creates a minimal boot environment for the initial thread, which 12 is started at priority \texttt{seL4\_MaxPrio} and maximum control priority \texttt{seL4\_MaxPrio}. 13This environment consists of the initial thread's TCB, CSpace and VSpace, 14consisting of frames that contain the userland image (code/data of the initial 15thread) and the IPC buffer. 16 17On the MCS kernel, the initial thread is configured with a round-robin scheduling context 18with \texttt{CONFIG\_BOOT\_THREAD\_TIME\_SLICE} milliseconds timeslice. 19Without MCS, all threads including the initial thread are scheduled round-robin with 20\texttt{CONFIG\_TIMER\_TICK\_MS} $*$ \texttt{CONFIG\_TIME\_SLICE} timeslices. 21 22The initial thread's CSpace consists of exactly one CNode 23which contains capabilities to the initial 24thread's own resources as well as to all available global resources. 25The CNode size can be configured at compile time (default is $2^{12}$ 26slots), but the guard is always chosen so that the CNode resolves exactly 27the number of bits in the architecture (32 bits or 64 bits). This means, the 28first slot of the CNode has CPTR 0x0, the second slot has CPTR 0x1 etc. 29 30The first 12 slots contain specific capabilities as listed in 31\autoref{tab:cnode_content}. 32 33\begin{table}[htb] 34 \begin{center} 35 \caption{Initial thread's CNode content.} 36 \label{tab:cnode_content} 37 \begin{tabularx}{\textwidth}{lX} 38 \toprule 39 Enum Constant & Capability \\ 40 \midrule 41 \texttt{seL4\_CapNull} & null \\ 42 \texttt{seL4\_CapInitThreadTCB} & initial thread's TCB \\ 43 \texttt{seL4\_CapInitThreadCNode} & initial thread's CNode \\ 44 \texttt{seL4\_CapInitThreadVSpace} & initial thread's VSpace \\ 45 \texttt{seL4\_CapIRQControl} & global IRQ controller (see \autoref{sec:interrupts}) \\ 46 \texttt{seL4\_CapASIDControl} & global ASID controller (see \autoref{ch:vspace}) \\ 47 \texttt{seL4\_CapInitThreadASIDPool} & initial thread's ASID pool (see \autoref{ch:vspace}) \\ 48 \texttt{seL4\_CapIOPort} & global I/O port cap, null cap if unsupported 49\ifxeightsix 50(see \autoref{sec:ioports}) 51\fi 52\\ 53 \texttt{seL4\_CapIOSpace} & global I/O space cap, null cap if unsupported 54\ifxeightsix 55(see \autoref{sec:iospace}) 56\fi 57\\ 58 \texttt{seL4\_CapBootInfoFrame} & BootInfo frame (see \autoref{ch:bootup:bootinfo}) \\ 59 \texttt{seL4\_CapInitThreadIPCBuffer} & initial thread's IPC buffer (see \autoref{sec:messageinfo}) \\ 60 \texttt{seL4\_CapDomain} & domain cap (see \autoref{sec:domains}) \\ 61 \texttt{seL4\_CapInitThreadSC} & initial thread's scheduling context (MCS only) \\ 62 \bottomrule 63 \end{tabularx} 64 \end{center} 65\end{table} 66 67\section{\label{ch:bootup:bootinfo}BootInfo Frame} 68 69CNode slots with CPTR \texttt{seL4\_NumInitialCaps} (defined in the seL4 70userland library) and above are filled dynamically during 71bootstrapping. Their exact contents depend on the userland image size, 72platform configuration (devices) etc. In order to tell the initial thread 73which capabilities are stored where in its CNode, the kernel provides 74a \emph{BootInfo Frame} which is mapped into the initial thread's address 75space. The mapped address is chosen by the kernel and given to the initial 76thread via a CPU register. 77 78The BootInfo Frame contains the C struct described in 79\autoref{tab:bootinfo_struct}. 80It is defined in the seL4 userland library. Besides talking about 81capabilities, it also informs the initial thread about 82the current platform's configuration. 83 84The type \texttt{seL4\_SlotRegion} is a C struct 85which contains \texttt{start} and \texttt{end} slot CPTRs. It denotes a region 86of slots in the initial thread's CNode, starting with CPTR \texttt{start} and with 87\texttt{end} being the CPTR of the first slot after the region ends, i.e.\ 88\texttt{end - 1} points to the last slot of the region. 89 90\begin{table}[htb] 91 \begin{center} 92 \caption{BootInfo struct.} 93 \label{tab:bootinfo_struct} 94 \begin{tabularx}{\textwidth}{llX} 95 \toprule 96 Field Type & Field Name & Description \\ 97 \midrule 98 \texttt{seL4\_Word} & \texttt{extraLen} & length of additional bootinfo information in bytes \\ 99 \texttt{seL4\_NodeId} & \texttt{nodeID} & node ID \\ 100 \texttt{seL4\_Word} & \texttt{numNodes} & number of nodes \\ 101 \texttt{seL4\_Word} & \texttt{numIOPTLevels} & number of I/O page-table levels (-1 if CONFIG\_IOMMU unset) \\ 102 \texttt{seL4\_IPCBuffer*} & \texttt{ipcBuffer} & pointer to the initial thread's IPC buffer \\ 103 \texttt{seL4\_SlotRegion} & \texttt{empty} & empty slots (null caps) \\ 104 \texttt{seL4\_SlotRegion} & \texttt{sharedFrames} & reserved \\ 105 \texttt{seL4\_SlotRegion} & \texttt{userImageFrames} & frames containing the userland image \\ 106 \texttt{seL4\_SlotRegion} & \texttt{userImagePaging} & userland-image paging structure caps \\ 107 \texttt{seL4\_SlotRegion} & \texttt{ioSpaceCaps} & I/O space capabilities for ARM SMMU \\ 108 \texttt{seL4\_SlotRegion} & \texttt{extraBIPages} & frames backing additional bootinfo information \\ 109 \texttt{seL4\_Uint8} & \texttt{initThreadCNodeSizeBits} & CNode size ($2^n$ slots) \\ 110 \texttt{seL4\_Word} & \texttt{initThreadDomain} & domain of the initial thread (see \autoref{sec:domains}) \\ 111 \texttt{seL4\_SlotRegion} & \texttt{schedcontrol} & seL4\_SchedControl capabilities, one for each node (MCS only). \\ 112 \texttt{seL4\_SlotRegion} & \texttt{untyped} & untyped-memory capabilities \\ 113 \texttt{seL4\_UntypedDesc[]} & \texttt{untypedList} & array of information about each untyped \\ 114 \bottomrule 115 \end{tabularx} 116 \end{center} 117\end{table} 118 119Depending on the architecture and platform there might be additional pieces of boot 120information. If \texttt{extraLen} is greater then zero then 4K after the start of bootinfo 121is a region of extraLen bytes containing additional bootinfo structures. Each chunk starts 122with a \texttt{seL4\_BootInfoHeader}, described in \autoref{tab:bi_header_struct}, that 123describes what the chunk is and how long it is, where the length includes the header. The 124length can be used to skip over chunks that you do not understand. The only generally 125defined chunk type is \texttt{SEL4\_BOOTINFO\_HEADER\_PADDING} and describes an empty 126chunk that has no data, any other types are platform or architecture specific. The 127\texttt{extraBIPages} slot region gives the frames capabilities for the pages that make up 128the additional boot info region. 129 130\begin{table}[htb] 131 \begin{center} 132 \caption{BootInfoHeader struct.} 133 \label{tab:bi_header_struct} 134 \begin{tabular}{lll} 135 \toprule 136 Field Type & Field Name & Description \\ 137 \midrule 138 \texttt{seL4\_Word} & \texttt{id} & Identifier indicating the contents of the chunk \\ 139 \texttt{seL4\_Uint8} & \texttt{len} & Length in bytes of the chunk \\ 140 \bottomrule 141 \end{tabular} 142 \end{center} 143\end{table} 144 145The capabilities in \texttt{userImageFrames} are 146ordered such that the first capability references the first frame of the 147userland image and so on. 148The capabilities in \texttt{userImagePaging} are ordered in descending order 149of paging structure size. Within a given paging structure size, capabilities are 150ordered by the virtual address at which the corresponding objects are mapped 151into the initial thread's address space. 152 153It is up to userland to infer the virtual address of frames referenced by 154the capabilities in \texttt{userImageFrames} and the virtual address and 155types of paging structures 156referenced by the capabilities in \texttt{userImagePaging}. 157Userland typically has a way of finding out to which virtual addresses its 158code and data is mapped (e.g.\ in GCC, with the standard linker script, the 159symbols \texttt{\_\_executable\_start} and \texttt{\_end} are available). 160Additionally, the initial thread can assume that its address space is virtually 161contiguous, and is made up of the smallest frames available on the architecture. 162It's also assumed that the initial thread knows which paging structures are 163available on the architecture it's running on. 164This, along with knowledge of how capabilities in \texttt{userImageFrames} and 165\texttt{userImagePaging} are ordered, is sufficient information for userland to infer 166the virtual address of each 167frame capability, and the virtual address and type of each paging structure capability. 168 169Untyped memory is given in no particular order. The array entry 170\texttt{untypedList[i]} stores the untyped-memory information of 171the i-th untyped cap of the slot region \texttt{untyped}. Therefore, the array 172length is at least \texttt{untyped.end - untyped.start}. The actual length is 173hardcoded in the kernel and irrelevant to the reader of the array. The untyped 174memory information is stored in a \texttt{seL4\_UntypedDesc} struct, described 175in \autoref{tab:untyped_desc_struct}, and details the address, size and kind of 176the memory backing the untyped. This allows userland to infer physical memory 177addresses of retyped frames and use them to initiate DMA transfers when no 178IOMMU is available. The kernel makes no guarantees about certain sizes of untyped 179memory being available. 180 181\begin{table}[htb] 182 \begin{center} 183 \caption{seL4\_UntypedDesc struct} 184 \label{tab:untyped_desc_struct} 185 \begin{tabular}{lll} 186 \toprule 187 Field Type & Field Name & Description \\ 188 \midrule 189 \texttt{seL4\_Word} & \texttt{paddr} & physical base address of the untyped object \\ 190 \texttt{seL4\_Uint8} & \texttt{sizeBits} & size ($2^n$ bytes) of the untyped object \\ 191 \texttt{seL4\_Uint8} & \texttt{isDevice} & is this untyped a device or not (see \autoref{sec:kernmemalloc}) \\ 192 \texttt{seL4\_Uint8[]} & \texttt{padding} & manual padding so final struct is a multiple of the word size \\ 193 \bottomrule 194 \end{tabular} 195 \end{center} 196\end{table} 197 198If the platform has an seL4-supported IOMMU, \texttt{numIOPTLevels} contains 199the number of IOMMU-page-table levels. This information is needed by userland 200when constructing an IOMMU address space (IOSpace). If there is no IOMMU 201support, \texttt{numIOPTLevels} is \texttt{0}. 202 203On ARM if the platform has any available SMMU units the capabilities for them 204will be described by the \texttt{ioSpaceCaps} slot region. The mapping of a 205capability from this region to a specific SMMU is platform specific. 206 207\ifxeightsix 208\section{Boot Command-line Arguments} 209 210On IA-32, seL4 accepts boot command-line arguments which are passed to the 211kernel via a multiboot-compliant bootloader (e.g.\ GRUB, syslinux). Multiple 212arguments are separated from each other by whitespace. Two forms of arguments 213are accepted: 214(1) key-value arguments of the form ``key=value'' and (2) single keys of the 215form ``key''. The value field of the key-value form may be a string, a decimal 216integer, a hexadecimal integer beginning with ``0x'', or an integer list where 217list elements are separated by commas. 218Keys and values can't have any whitespace in them and there can be no 219whitespace before or after an ``='' or a comma either. 220Arguments are listed in \autoref{tab:bootargs} along with their default values (if left unspecified). 221 222 223\begin{table}[htb] 224 \caption{IA-32 boot command-line arguments.} 225 \begin{tabularx}{\textwidth}{lXX} 226 \toprule 227 Key & Value & Default \\ 228 \midrule 229 \texttt{console\_port} & 230 I/O-port base of the serial port that the kernel prints to 231 (if compiled in debug mode) & 232 0x3f8 \\ 233 \texttt{debug\_port} & 234 I/O-port base of the serial port that is used for kernel debugging 235 (if compiled in debug mode) & 236 0x3f8 \\ 237 \texttt{disable\_iommu} & 238 none & 239 The IOMMU is enabled by default on VT-d-capable platforms \\ 240 \bottomrule 241 \end{tabularx} 242 \label{tab:bootargs} 243\end{table} 244\fi 245