sel4源码解析（一） - sel4内核对象
sel4是微内核，它只提供了少数供用户程序使用的机制。不像linux内核提供了大量的服务。本文主要介绍sel4提供的七个内核对象，着重讲述了untyped这一内核对象。
sel4内核对象
Sel4提供了七个内核对象，这七个内核对象构成了一个进程基本运行环境。它们分别是：
-
CNodes：CNodes本质是一个结构体数组，该数组的元素是cte（capability table entry），该cte中包含一个cap_t结构体和mdb_node_t结构体（todo）。一个进程的CNodes称为Cspace，CNodes的cte称为slot。
-
Thread Control Blocks：同一般的进程控制块类似，表示一个进程的运行状态；
-
Endpoints：类似于记录型信号量。进程1想要receive信息，但进程2还未send该信息，导致进程1暂时被挂载在该Endpoints队列上。一旦进程2 send该信息，则将进程1从该endpoints队列上取出，并重新加入调度队列；
-
Notification：sel4实现的通知机制，让进程之间可以使用notification完成同步；
-
Virtual address space：进程的虚拟地址空间；
-
Interrupt ：
-
Untyped：
untyped
sel4 untyped表示为一块连续未分配的物理内存，用户程序可以通过untyped cap来使用这块物理内存。下面介绍了untyped cap结构体以及在untyped内存上创建TCB内核对象。
untyped cap结构体
untyped cap结构体：
- capFreeIndex：表示起始空闲地址的偏移；
- capIsDevice：表示当前这段连续的物理内存是否为设备地址空间；
- capBlockSize：表示当前这段连续的物理内存空间大小；
- capPtr：指向当前这段连续的物理内存起始地址。
capFreeIndex和capPtr的区别是：untyped的内存可能有一部分被使用了，应为capFreeIndex表示当前的untyped空闲内存，所以capFreeIndex会随之改变。而capPtr表示untyped物理内存起始地址，所以capPtr不会改变。
block untyped_cap {
field capFreeIndex 48 // 起始空闲地址的偏移
padding 9
field capIsDevice 1
field capBlockSize 6
field capType 5
padding 11
field_high capPtr 48 // untyped的内存起始地址
}
创建内核对象TCB
seL4_Untyped_Retype函数是使用untyped的物理内存的唯一API，其有八个参数，分别是：
- seL4_Untyped _service：untyped的cap；
- seL4_Word type：创建的内核对象类型，本例是seL4_TCBObject；
- seL4_Word size_bits:创建内核对象所占内存的大小，这里TCB是固定的（由Kernel指定），故为0；
- seL4_CNode root：CNode的基地址；
- seL4_Word node_index：
- seL4_Word node_depth：
- seL4_Word node_offset：存放在CNode表中的untyped cap的偏移；
- seL4_Word num_objects：将要创建的内核对象cap的个数。
具体的创建流程如下：
- 用户程序调用函数seL4_Untyped_Retype；
seL4_Untyped_Retype(child_untyped, seL4_TCBObject, 0, seL4_CapInitThreadCNode, 0, 0, child_tcb, 1);
-
进入内核，根据系统调用编号，执行decodeUntypedInvocation函数。该函数执行的操作如下：
a. 从ipc buffer里面取出创建内核对象的相关信息；
b. 根据root、node_index和node_depth找到对应的CNode cap；
c. 检查该CNode的尺寸是否容得下node_offset以及对应node_offset的slot是否为空；
d. 根据untyped cap信息得到untyped内存的空间内存的起始地址，并判断是否能够存放内核对象；
e. 调用invokeUntyped_Retype函数。 -
invokeUntyped_Retype函数更新该untyped cap存放的空闲内存信息，并调用createNewObjects函数；
-
createNewObjects函数的功能如下：
a. 在untyped cap指向的空闲空间初始化tcb；
b. 生成tcb cap；
c. 将该tcb cap插入到第2步找到得的CNode对应的slot里。 -
完成。
相关阅读
sel4源码解析（一） - sel4内核对象
sel4源码解析（二） - CSpace
sel4源码解析（三） - sel4系统调用处理流程
sel4源码解析（四） - ipc
sel4源码解析（五） - Notification
sel4源码解析（六） - 进程
sel4源码解析（七） - vspace