内核对象与 Capability机制 #
ReL4继承了seL4对内核对象的定义和管理，提供了7种基本的内核对象：
- 线程（Thread）：内核调度的基本单位，保存了用户态运行的上下文寄存器。
- 能力空间（CNode）：权限控制负责，维护了各个内核对象的能力对象和对应权限。
- 内存页（Frame）：可访问的物理内存块。
- VSpace（PageTable）：地址空间，维护了
- 端点（Endpoint）：同步IPC的桥梁，维护了一个消息收发的状态机以及对应的阻塞队列。
- 通知对象（Notification）：异步通知机制的桥梁，维护了一个通知状态位。
- 未初始化的内存对象（Untyped）：通过系统调用转化为其他内核对象。
What’s a capability #
A capability is a unique, unforgeable token that gives the possessor permission to access an entity or object in system.
按照seL4文档定义，可以理解为 capability 是访问系统中一切实体或对象的令牌，这个令牌包含了某些访问权力，只有持有这个令牌，才能按照特定的方式访问系统中的某个对象。可以将 capability 视为一个拥有访问权限的指针，而在C语言中，指针常常可以共享，因此这里隐含着一层 capability 可以传递和分享的意思。
seL4 中将 capability 分做三种：
- 内核对象（如 线程控制块）的访问控制的
capability。 - 抽象资源（如
IRQControl）的访问控制的capability。（中断控制块是干啥的，以后会提到） untyped capabilities，负责内存分配的capabilities。seL4不支持动态内存分配，在内核加载阶段将所有的空闲内存绑定到untyped capabilities上，后续的内核对象申请新的内存，都通过系统调用和untyped caability来申请。 在seL4内核初始化时，指向内核控制资源的所有的capability全部被授权给特殊的任务root task，用户代码向修改某个资源的状态，必须使用kernel API在指定的capability上请求操作。
关于 Root Task，有几个概念上的疑惑问答，参考： About Root Task in seL4
CNodes and CSlots #
A CNode (capability-node) is an object full of capabilities: you can think of a CNode as an array of capabilities.
简单来说， CNode 也是一个对象，但这个对象存的是一个数组，数组里的元素是 capability 。数组中的各个位置我们称为 CSlots ，在上面的例子中， seL4_CapInitThreadTCB 实际上就是一个 CSlot ，这个 CSlot 中存的是控制 TCB 的 capability 。
每个 Slot 有两种状态：
empty：没有存capability。full：存了capability。
出于习惯，0号 Slot 一直为 empty。
一个 CNode 有 1 << CNodeSizeBits 个 Slot，一个 Slot 占 1 << seL4_SlotBits 字节。
CSpaces #
CSpace 是一个 线程 的能力空间，包含一个或多个CNode，构造出一个能力空间的树形结构。
CSpace的寻址方式有两种：
- Invocation
- Direct CSpace addressing
Invocation Addressing #
每个线程有在 TCB 中装载了一个特殊的 CNode 作为它 CSpace 的 root。这个 root 可以为空（代表这个线程没有被赋予任何 capability ）。
在 Invocation 方式中，我们通过隐式地调用线程的 CSpace root 来寻址 CSlot 。例如：我们使用对 seL4_CapInitThreadTCB CSlot 的调用来读取和写入由该特定 CSlot 中的功能表示的 TCB 的寄存器。
这个模式会在 CSpace root 中隐式地查找 seL4_CapInitThreadTCB Slot 。
Direct CSpace addressing #
与 Invocation 默认在 CSpace root 中查找不同，你可以指定你要在哪个 CNode 中查找。这种操作主要用于构建和操作 CSpace 的形状（可能是另一个线程的 CSpace ）。
Capability派生 #
capability可以通过若干系统调用（如Copy、Mint、retype等）进行能力派生，派生出来的新的cap作为原始cap的子节点插入能力派生树中。
能力派生树与CSpace是不同的概念。CSpace是一个线程中可以操作的内核对象的cap集合。而能力派生树则是以某一个cap（往往是untyped cap）为根节点，维护和管理系统中所有cap的生命周期的数据结构，由整个系统共享。
Untyped #
除了一小部分静态的内核内存，seL4 所有的物理内存都在用户态被管理。在启动时由 seL4 创建root task持有的内核对象的 capability ，以及由 seL4 管理的其他的物理资源，在启动后都会传递给 root task。除了用于创建 root task 的对象之外，所有可用的物理内存的 capability 都作为 untyped memory 的 capability 传递给 root task。
Untyped memory 是一块特定大小的连续物理内存块，而 untyped capabilities 则是 untyped memory 的 capability。 untyped capabilities 可以被 retyped 。
untyped capabilities 有一个 bool 的属性，指明对应的内存对象是否可以被内核写：内存对象可能不是 RAM 而是其他 Device，或者它可能位于内核无法寻址到的 RAM 区域。
只要untyped capability对应的memory大小允许，memory可以被拆分成许多新的object。使用seL4_Untyped_Retype函数对untyped capability进行创建新的capability（同时也是会对应的untyped object进行retype）。新的capability是原来untyped capability的children，children按顺序获得有效内存，且内存是对齐的。例如，创建4k object以后创建16k object，这样有12k就被浪费了。
Interface #
seL4_CNode_Copy：复制cap，同时设置其访问权限。seL4_CNode_Delete：删除一个cap。seL4_CNode_Mint：复制cap，同时设置权限及徽章（badge）。seL4_CNode_Move：移动一个cap。seL4_CNode_Revoke：删除所有派生出去的cap。seL4_Untyped_Retype：从untyped对象中生成一个新的内核对象。