Sel4系统引导概念介绍
1， 初始化线程的环境
Sel4内核为初始化线程创建一个最小的引导环境，环境中包括初始化线程的TCB,Cspace,Vspace.还包括用户空间image(初始化线程的code/data)以及IPC缓存。电脑初始化线程的Cspace只有一个CNODE, 他使得初始化线程既可以访问自有的资源也可以访问其他的全局资源。CNODE的大小可以在编译的时候配置（默认是2的12次方 slots）,
但是因为第0个CPTR总是被用来做保护（CNODE可以精确的处理32bits），这其实意味着，数字序号上的第一个slot 占用的CPTR 0，数字序号上的第2个slot占用CPTR 1
初始化线程的CNode的内容
enum {
seL4_CapNull = 0, /* null cap */
seL4_CapInitThreadTCB = 1, /* initial thread's TCB cap */
seL4_CapInitThreadCNode = 2, /* initial thread's root CNode cap */
seL4_CapInitThreadVSpace = 3, /* initial thread's VSpace cap */
seL4_CapIRQControl = 4, /* global IRQ controller cap */
seL4_CapASIDControl = 5, /* global ASID controller cap */
seL4_CapInitThreadASIDPool = 6, /* initial thread's ASID pool cap */
seL4_CapIOPort = 7, /* global IO port cap (null cap if not supported) */
seL4_CapIOSpace = 8, /电脑 * global IO space cap (null cap if no IOMMU support) */
seL4_CapBootInfoFrame = 9, /* bootinfo frame cap */
seL4_CapInitThreadIPCBuffer = 10, /* initial thread's IPC buffer frame cap */
seL4_CapDomain = 11, /* global domain controller cap */
seL4_NumInitialCaps = 12
};
2， BootInfo Frames 引导信息
seL4 userland library 定义了CPTR seL4 NumInitialCaps 他是CNode slots。他在系统引导过程中被动态填充，他们确切大小取决于userland image size，以及平台配置的设备等等。内核提供了一个BootInfo Frame 映射到初始化线程的地址空间，这样可以告诉初始化线程他的CNode中包含哪些功能权限，内核决定映射的地址，然后直接通过CPU register 告诉初始化线程。初始化线程通过seL4 GetBootInfo()来访问这个地址。
BootInfo Frames 的C struct 在seL4 userland library中定义。BootInfo Frames中除了定义了功能权限以外还包括当前平台的的配置信息。
seL4 SlotRegion 是一个C struct 它包括start and end slot CPTRs，他表示初始化线程的slots的一个区域。从CPTR start开始，结束在slot区域后的第一个slot。
userImageFrames中的功能权限（capabilities）都已经定义好的。
userImagePaging中的功能权限（capabilities）按分页结构大小的降序进行排序。
在给定的分页结构大小内，功能按相应对象映射到初始线程地址空间的虚拟地址进行排序。由userland推导 userImageFrames 中的功能权限（capabilities）的frames的虚拟地址，同时userImageFrames 中的功能权限（capabilities）会引用虚拟地址和页结构类型。Userland 通常会有办法找到其代码和数据映射的虚拟地址（. in GCC, with the standard linker script, the symbols executable start and end are available）。
另外，初始化线程假定他的地址空间是连续的虚拟地址，并且他们是由平台架构上允许的最小的frames组成，同样假定初始化线程知道那种分页结构适合正在运行的平台架构。这些信息以及 userImageFrames and userImagePaging中的功能权限（capabilities）是如何排列的，是必要的信息，对于userland去推断每一个功能权限（capabilities）的frame的虚拟地址，以及每个一个页结构体的类型和虚拟地址。
非类型化内存没有特定的顺序。untypedSizeBitsList[i]数组存储槽区域的第i个非类型化cap的非类型化内存的大小。Therefore, the array length is at least untyped.end - untyped.start. 实际长度是在内核中硬编码的，与数组的读取器无关。数组untypedPaddrList也是这样的。对于每个非类型化内存cap，它可以存储非类型化内存数据到物理地址。这使得userland可以重新格式化frames的物理内存地址，并且在没有IOMMU可用时，使用他们初始化DMA传送器。除非内核提供编译时可配置的最少4K的非类型化capabilities，否则内核并不能保证有特定大小的非类型化内存可用。
内核创建与内存映射设备相关联的每个物理内存区域的frames。这些设备区域要么是编码的(例如，在嵌入式平台上)，要么是内核在引导时通过PCI总线扫描发现的。每个区域的物理基地址存储在BasePaddr中。槽区域帧标识用于支持该区域的所有帧上限。它们是有序的，因此该区域的第一帧由该插槽区域中的第一个CAP引用，并由物理地址BasPaddr支持。所有帧都具有相同的大小：2FrameSizeBits字节。因此，整个区域的大小是(frames.end - frames.start) << frameSizeBits.
BootInfo结构的数组deviceRegions存储所有可用的设备区域(即它们的结构)。阵列中NumDeviceRegion代表整个阵列中可用的数量。
如果平台具有seL4支持的IOMMU，则numIOPTLeveles包含IOMMU-page-table的levels数量。Userland在构建IOMMU地址空间(IOSpace)时需要此信息。如果不支持IOMMU，则number IOPTLeveles为0。
typedef struct {
seL4_NodeId nodeID; /* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */
seL4_Word numNodes; /* number of seL4 nodes (1 if uniprocessor) */
seL4_Word numIOPTLevels; /* number of IOMMU PT levels (0 if no IOMMU support) */
seL4_IPCBuffer* ipcBuffer; /* pointer to initial thread's IPC buffer */
seL4_SlotRegion empty; /* empty slots (电脑null caps) */
seL4_SlotRegion sharedFrames; /* shared-frame caps (shared between seL4 nodes) */
seL4_SlotRegion userImageFrames; /* userland-image frame caps */
seL4_SlotRegion userImagePaging; /* userland-image paging structure caps */
seL4_SlotRegion untyped; /* untyped-object caps (untyped caps) */
seL4_SlotRegion ioSpaceCaps; /* IOSpace caps for ARM SMMU */
seL4_PAddr untypedPaddrList [CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* physical address of each untyped cap */
seL4_Uint8 untypedSizeBitsList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* size (2^n) bytes of each untyped cap */
seL4_Uint8 initThreadCNodeSizeBits; /* initial thread's root CNode size (2^n slots) */
seL4_Word numDeviceRegions; /* number of device regions */
seL4_DeviceRegion 电脑deviceRegions[CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS]; /* device regions */
seL4_Domain initThreadDomain; /* Initial thread's domain ID */
} seL4_BootInfo;
3， Boot Command-line Arguments 引导命令行参数
在IA-32上，seL4接受引导命令行参数，这些参数通过兼容多重引导的引导加载程序(例如GRUB、syslinux)传递给内核。多个参数之间用空格隔开。接受两种形式的参数：(1)“key=Value”形式的键值参数和(2)“key”形式的单键。
键值形式的值字段可以是字符串、十进制整数、以“0x”开头的十六进制整数或列表元素由逗号分隔的整数列表。键和值中不能有任何空格，“=”或逗号前后也不能有空格。表9.4中列出了参数及其缺省值(如果未指定)。
4， Multikernel Bootstrapping 多核启动过程
在ARM上，seL4仅支持单处理器，不支持多内核[BBD+09]引导。因此，BootInfo结构的字段nodeID将始终为0，numNodes将为1，而sharedFrames将为空区域。
在IA-32上，通过将启动命令行参数max num nodes设置为大于1的值，可以将seL4作为多内核进行引导。然后，每个可用的CPU核心将运行seL4的一个独立节点，直到指定的最大数量。可用物理内存在节点之间平均分区。所有设备帧都将提供给所有节点。节点的初始线程必须协调对这些设备帧的访问，例如通过定义哪个节点负责哪个设备。IOMMU管理只能由第一个节点执行，其他节点不具有全局IOSpace功能。还有在编译时定义的节点数的硬上限(默认为8，但可以增加到256)。电脑
除共享帧外，节点彼此隔离。在引导时，内核创建多个4K userland frames，这些帧在节点之间共享。这个数字可以通过启动命令行参数num sh Frame进行配置。共享帧将出现在每个节点的初始线程的CNode中。它们以相同的顺序分配给每个初始线程。在BootInfo结构中，字段sharedFrames包含它们的槽区域。
用户可以使用共享帧来实现共享数据结构、消息传递和同步机制。例如，可以铸造单个帧并将其分发给子系统。这允许以细粒度的方式跨节点连接它们。每个节点都有一个节点ID(BootInfo中的字段nodeID)，而可以从字段NumNodes中获取节点数。
与多重引导兼容的引导加载程序(例如GRUB、syslinux)通过引导模块将用户区域镜像提供给内核。每个引导模块都包含一个用户区域镜像的ELF文件。如果只有一个Userland镜像，则每个节点都将获得该Userland镜像的自己的副本。如果给定了多个用户区域镜像，则第一个节点获取第一个镜像，第二个节点获取第二个镜像，依此类推。如果节点多于镜像，则剩余的每个节点将获取最后一个镜像的副本。
如果内核是在调试模式下编译的，则可以为每个节点分配一个单独的控制台端口和调试端口，这可以通过指定I/O端口基址数组来完成。例如，控制台端口=0x3f8，0x2f8，0x3e8，0x2e8将端口0x3f8分配给节点0，将端口0x2f8分配给节点1，依此类推。其余节点没有分配的端口，也不会产生控制台输出。参数调试端口的工作方式与此完全相同。
电脑