manual/parts/bootup.tex

19 Without MCS, all threads including the initial thread are scheduled round-robin with
70 userland library) and above are filled dynamically during
73 which capabilities are stored where in its CNode, the kernel provides
126 chunk that has no data, any other types are platform or architecture specific. The
145 The capabilities in \texttt{userImageFrames} are
146 ordered such that the first capability references the first frame of the
148 The capabilities in \texttt{userImagePaging} are ordered in descending order
149 of paging structure size. Within a given paging structure size, capabilities are
150 ordered by the virtual address at which the corresponding objects are mapped
159 symbols \texttt{\_\_executable\_start} and \texttt{\_end} are available).
162 It's also assumed that the initial thread knows which paging structures are
165 \texttt{userImagePaging} are ordered, is sufficient information for userland to infer
210 On IA-32, seL4 accepts boot command-line arguments which are passed to the
212 arguments are separated from each other by whitespace. Two forms of arguments
213 are accepted:
214 (1) key-value arguments of the form ``key=value'' and (2) single keys of the
217 list elements are separated by commas.
220 Arguments are listed in \autoref{tab:bootargs} along with their default values (if left unspecified).