manual/parts/bootup.tex

11 The seL4 kernel creates a minimal boot environment for the initial thread, which
13 This environment consists of the initial thread's TCB, CSpace and VSpace,
14 consisting of frames that contain the userland image (code/data of the initial
15 thread) and the IPC buffer.
17 On the MCS kernel, the initial thread is configured with a round-robin scheduling context
19 Without MCS, all threads including the initial thread are scheduled round-robin with
23 which contains capabilities to the initial
26 slots), but the guard is always chosen so that the CNode resolves exactly
27 the number of bits in the architecture (32 bits or 64 bits). This means, the
28 first slot of the CNode has CPTR 0x0, the second slot has CPTR 0x1 etc.
69 CNode slots with CPTR \texttt{seL4\_NumInitialCaps} (defined in the seL4
71 bootstrapping. Their exact contents depend on the userland image size,
72 platform configuration (devices) etc. In order to tell the initial thread
73 which capabilities are stored where in its CNode, the kernel provides
74 a \emph{BootInfo Frame} which is mapped into the initial thread's address
75 space. The mapped address is chosen by the kernel and given to the initial
78 The BootInfo Frame contains the C struct described in
80 It is defined in the seL4 userland library. Besides talking about
81 capabilities, it also informs the initial thread about
82 the current platform's configuration.
86 of 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.
102       \texttt{seL4\_IPCBuffer*}     & \texttt{ipcBuffer}               & pointer to the initial thread's IPC buffer \\
105       \texttt{seL4\_SlotRegion}     & \texttt{userImageFrames}         & frames containing the userland image \\
110       \texttt{seL4\_Word}           & \texttt{initThreadDomain}        & domain of the initial thread (see \autoref{sec:domains}) \\
119 Depending on the architecture and platform there might be additional pieces of boot
120 information. If \texttt{extraLen} is greater then zero then 4K after the start of bootinfo
123 describes what the chunk is and how long it is, where the length includes the header. The
127 \texttt{extraBIPages} slot region gives the frames capabilities for the pages that make up
128 the additional boot info region.
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 \\
146 ordered such that the first capability references the first frame of the
150 ordered by the virtual address at which the corresponding objects are mapped
151 into the initial thread's address space.
153 It is up to userland to infer the virtual address of frames referenced by
154 the capabilities in \texttt{userImageFrames} and the virtual address and
156 referenced by the capabilities in \texttt{userImagePaging}.
158 code and data is mapped (e.g.\ in GCC, with the standard linker script, the
160 Additionally, the initial thread can assume that its address space is virtually
161 contiguous, and is made up of the smallest frames available on the architecture.
162 It's also assumed that the initial thread knows which paging structures are
163 available on the architecture it's running on.
166 the virtual address of each
167 frame capability, and the virtual address and type of each paging structure capability.
170 \texttt{untypedList[i]} stores the untyped-memory information of
171 the i-th untyped cap of the slot region \texttt{untyped}. Therefore, the array
173 hardcoded in the kernel and irrelevant to the reader of the array. The untyped
175 in \autoref{tab:untyped_desc_struct}, and details the address, size and kind of
176 the memory backing the untyped. This allows userland to infer physical memory
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 \\
192       \texttt{seL4\_Uint8[]} & \texttt{padding} & manual padding so final struct is a multiple of the word size \\
198 If the platform has an seL4-supported IOMMU, \texttt{numIOPTLevels} contains
199 the number of IOMMU-page-table levels. This information is needed by userland
203 On ARM if the platform has any available SMMU units the capabilities for them
204 will be described by the \texttt{ioSpaceCaps} slot region. The mapping of a
210 On IA-32, seL4 accepts boot command-line arguments which are passed to the
214 (1) key-value arguments of the form ``key=value'' and (2) single keys of the
215 form ``key''. The value field of the key-value form may be a string, a decimal
230             I/O-port base of the serial port that the kernel prints to
234             I/O-port base of the serial port that is used for kernel debugging