manual/parts/bootup.tex

12  is started at priority \texttt{seL4\_MaxPrio} and maximum control priority \texttt{seL4\_MaxPrio}.
17 On the MCS kernel, the initial thread is configured with a round-robin scheduling context
25 The CNode size can be configured at compile time (default is $2^{12}$
26 slots), but the guard is always chosen so that the CNode resolves exactly
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
80 It is defined in the seL4 userland library. Besides talking about
84 The type \texttt{seL4\_SlotRegion} is a C struct
120 information. If \texttt{extraLen} is greater then zero then 4K after the start of bootinfo
121 is a region of extraLen bytes containing additional bootinfo structures. Each chunk starts
123 describes what the chunk is and how long it is, where the length includes the header. The
125 defined chunk type is \texttt{SEL4\_BOOTINFO\_HEADER\_PADDING} and describes an empty
153 It is up to userland to infer the virtual address of frames referenced by
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.
165 \texttt{userImagePaging} are ordered, is sufficient information for userland to infer
169 Untyped memory is given in no particular order. The array entry
172 length is at least \texttt{untyped.end - untyped.start}. The actual length is
174 memory information is stored in a \texttt{seL4\_UntypedDesc} struct, described
178 IOMMU is available. The kernel makes no guarantees about certain sizes of untyped
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 \\
199 the number of IOMMU-page-table levels. This information is needed by userland
200 when constructing an IOMMU address space (IOSpace). If there is no IOMMU
201 support, \texttt{numIOPTLevels} is \texttt{0}.
205 capability from this region to a specific SMMU is platform specific.
234             I/O-port base of the serial port that is used for kernel debugging
239             The IOMMU is enabled by default on VT-d-capable platforms \\