seL4 Capabilities（翻自官网）（一）

官网教程链接: Capability

初始化Capabilities tutorials

// 先使用repo拉取一下tutorials，然后执行repo sync，所有的教程都在里面，学习某个的时候只需要改变的是 --tut 后面的参数
./init --tut capabilities
# building the tutorial exercise
cd capabilities_build
ninja

什么是Capability?

简单的讲是一个访问系统中实体或者对象的凭证（token），可以将其简单理解为是一个访问权限的指针，再seL4中有三种capabilities。

• 控制访问内核对象的，例如TCB（thread control blocks）
• 控制访问抽象资源的，例如IRQControl（Interrupt Requests, IRQ）
• 未分类能力

seL4中，初始化时，由内核控制的资源的能力赋予给根任务。若用户代码想要改变任何资源的状态，则可以使用内核API，可在libsel4中请求对特定能力指向的资源进行操作。
举例而言，根任务初始化的时候会携带一个指向它自己线程控制块（TCB）的能力，也即是 seL4_CapInitThreadTCB，其是一个由libsel4定义的常量。若想改变初始TCB的属性，则可以在该能力上使用TCB API中的任何方法。
下面是一个更改根任务TCB栈指针的例子，如果需要一个更大的栈则需要以下的操作：

// 这两行不懂，先扔这吧
seL4_UserContext registers;
seL4_Word num_registers = sizeof(seL4_UserContext)/sizeof(seL4_Word);

/* Read the registers of the TCB that the capability in seL4_CapInitThreadTCB grants access to. */
seL4_Error error = seL4_TCB_ReadRegisters(seL4_CapInitThreadTCB, 0, 0, num_registers, &registers);
assert(error == seL4_NoError);

/* set new register values */
registers.sp = new_sp; // the new stack pointer, derived by prior code.

/* Write new values */
error = seL4_TCB_WriteRegisters(seL4_CapInitThreadTCB, 0, 0, num_registers, &registers);
assert(error == seL4_NoError);

seL4_TCB_ReadRegisters和seL4_TCB_WriteRegisters的第一个参数指向seL4_CapInitThreadTCB插槽中的能力（capability）的地址。之后会解释地址(address)和插槽（slots）。剩余的参数是此次调用中特定的，进一步的解释可以查API。

CNodes和CSlots

一个CNode是一个装满能力的对象，可以将其理解为一个能力数组。将插槽（slot）称为功能插槽（capability-slots）。在上面的例子中，seL4_CapInitThreadTCB是根任务的CNode的插槽，该CNode包含着根任务TCB的能力。每个CNode中的插槽可能有如下状态：

• empty：插槽中没有能力
• full：包含一个指向内核资源的能力

按照惯例（by convention），0号插槽一般是空的，类似于在进程虚拟地址空间中将NULL标识未分配或者无效的内存位置一样，是为了避免在不小心使用未初始化的槽位时出现错误。
info->CNodeSizeBits字段给出了初始CNode大小的度量：它将会有1<<CNodeSizeBits个插槽（2^{CNodeSizeBits})。一个插槽有1<<seL4_SlotBits(2^{seL4_SlotBits})个字节，所以一个CNode的大小未2^{CNodeSizeBits+seL4_SlotBits}个字节。

CSpace

CSpace指的是能力空间，也就是一个线程中所有可访问的能力，可能是由一个或者多个CNodes组成的。在这一篇教程中，我们主要集中于由seL4的初始化协议为根任务构建的能力空间，是由一个CNode组成的。

CSpace addressing

为了引用一个能力且利用其执行操作，你必须要对其进行定位。在seL4 API中有两种方式对能力进行寻址。首先是通过调用，其次是通过直接寻址。调用是一种简写，我们用它来操作根任务TCB的寄存器（registers），下面是对其的进一步解释。

Invocation 调用

每个线程在其TCB中都有一个特殊的CNode能力，该能力作为其能力空间的根。这个根可以是空的（不包含任何能力），例如这个线程没有被授权调用任何能力，或者这个根节点也可以指向一个CNode，线程就可以使用其指向的那个CNode中的能力，这样该线程就可以在他的CSpace中管理和使用其他能力。
在一次invocation中，是通过隐式的调用执行该调用的线程的能力空间根来寻址能力插槽的。在上面的例子中，我们使用seL4_CapInitThreadTCB CSlot的调用，来读取和写入由该特定CSlot中的能力所表示的TCB（线程控制块）的寄存器。

seL4_TCB_WriteRegisters(seL4_CapInitThreadTCB, 0, 0, num_registers, &registers);

这会隐式的查询“调用线程能力空间根能力指向的CNode”（真他妈拗口）中的seL4_CapInitThreadTCB CSlot，这里指的就是根任务。
在某些情况下，当上下文足够清晰且其他信息不重要时，我们有时会用能力（capability）来代指它所指向的对象。比如，代替说“由 CSpace 根能力指向的 CNode”，我们有时会直接说“CSpace 根（其实是个能力）”。但如果不确定，最好还是保持精确。就像 C 语言中的结构体（structs）和指针（pointers）一样，对象（object）和能力（capabilities）并不是完全可互换的：一个对象可以被多个能力指向，而这些能力可能对该对象具有不同的权限级别。

能力空间直接寻址

对比起调用寻址，直接寻址允许你指定CNode进行查找能力，而不是隐式的使用能力空间根。这种方式主要用于构造和操作CSpaces的结构——可能是其他线程的CSpace。需要注意的式直接寻址也需要调用：这个操作需要调用一个CNode能力，而这个能力本身是从CSpace root索引的（搁着套娃呢）。
当对插槽进行直接寻址的时候，以下字段会被用到：

• _service/root CNode操作的能力
• index CNode地址中插槽的索引
• depth 在解析出CSlot之前要遍历CNode多远

对于初始的，单一级别的能力空间，depth的值总是seL4_WordBits。对于调用而言，depth默认的就是seL4_WordBits。为了将会对该值进行更多的讨论。
在下面的例子中，我们直接寻址根任务的TCB然后将其进行复制到能力空间根中的0号插槽位置（其实是将一个指向TCB的能力复制到另外一个插槽中去）。CNode复制需要两个直接寻址的插槽，为什么称为CNode复制而不叫slot复制呢？因为在进行能力复制的时候实际上实在CNode中操作能力槽，而且slot只是CNode中的一个元素，用于存储能力。复制能力的过程不仅仅是复制槽内容，而是需要操作整个CNode中的多个槽来完成复制，所以称为CNode复制更为合适。需要寻址的两个插槽，一个是目标插槽，另外一个是源插槽。seL4_CapInitThreadCNode的三种角色：

1. 源根(source root)：seL4_CapInitThreadCNode被用作源根，因为我们在同一个CNode中进行复制——即初始线程的CNode
2. 目标根（destination root），seL4_CapInitThreadCNode也被用作目标根，复制操作发生在同一个CNode内部
3. 源插槽（source slot），seL4_CapInitThreadCNode 被用作源插槽，因为在初始线程的 CNode 内，seL4_CapInitThreadCNode 是我们想要复制的能力所在的插槽（而 0号插槽是目标）。

 seL4_Error error = seL4_CNode_Copy(
    seL4_CapInitThreadCNode, 0, seL4_WordBits, // destination root, slot, and depth
    seL4_CapInitThreadCNode, seL4_CapInitThreadTCB, seL4_WordBits, // source root, slot, and depth
    seL4_AllRights);
assert(error == seL4_NoError);

所有的CNode调用都需要直接能力空间寻址。

初始化能力空间

根任务的能力空间是由seL4在启动时设置的，包含了由seL4管理的所有资源能力。我们已经看到了在根能力空间的几个能力：seL4_CapInitThreadTCB以及seL4_CapInitThreadCNode。这些都是在libsel4中由常量指定的，但是并不是所有的初始能力都是静态指定的。其他能力由libsel4中的seL4_BootInfo数据结构进行解释，由seL4进行初始化。seL4_BootInfo描述了初始能力的范围，包括了初始能力空间中的可用的插槽。

实操

zjx@in-container:/host$ ./init --tut capabilities

执行成功后是这样的

看一眼capabilities教程的源码

//使用qemu仿真硬件，./simulate进行执行，执行结果如下所示
./simulate

可以看到其中的主要内容是：

Booting all finished, dropped to user space
Initial CNode is 65536 slots in size
The CNode is 0 bytes in size
<<seL4(CPU 0) [decodeInvocation/646 T0xffffff801fe08400 "rootserver" @4013be]: Attempted to invoke a null cap #65535.>>
main@main.c:31 [Cond failed: error]
	Failed to set priority

运行时所有的输出都是有意义的。但是现在而言，第一行的输出信息来自内核，第二行的输出信息告诉你初始化CNode有多少个插槽。第三行则阐述了CSpace空间的大小，但是可以看出第三行的输出是错误的，现在的首要任务是将其改为对的。
从源码中可以看到：

 size_t initial_cnode_object_size_bytes = 0; // TODO calculate this.
 printf("The CNode is %zu bytes in size\n", initial_cnode_object_size_bytes);

根据上面理论上的内容来看，想要计算出CSpace（即此处的一个CNode的大小）还需要知道一个值，也就是seL4_SlotBits，也就是插槽的size_bits，根据下表可以看出，针对某一个对象的大小有两种表达方式Size in Bytes = 2^size_bits，为此查询了seL4的手册，发现如下表：

而我的qemu仿真的是x86-64，因此此处的seL4_SlotBits的值位5，每个插槽也就占了2⁵个字节，因此可以将上面的程序更改如下：

#define seL4_SlotBits 5
 size_t initial_cnode_object_size_bytes = BIT(info->initThreadCNodeSizeBits + seL4_SlotBits); // TODO calculate this.
 printf("The CNode is %zu bytes in size\n", initial_cnode_object_size_bytes);

修改之后可以看到输出：

这里看到，下面的输出有一个报错，“尝试调用了一个空能力，可以看到是未能设置优先级”,修改代码如下所示：

seL4_CPtr last_slot = info->empty.end - 1;
 /* TODO use seL4_CNode_Copy to make another copy of the initial TCB capability to the last slot in the CSpace */
 error = seL4_CNode_Copy(seL4_CapInitThreadCNode, last_slot, seL4_WordBits, 
                         seL4_CapInitThreadCNode, seL4_CapInitThreadTCB, seL4_WordBits,
                         seL4_AllRights);
 ZF_LOGF_IF(error, "Failed to copy cap!");
 /* set the priority of the root task */
 error = seL4_TCB_SetPriority(last_slot, last_slot, 10);
 ZF_LOGF_IF(error, "Failed to set priority");

这里有一些需要说明的点，info这个指针指向的对象里面到底都有什么？如下图所示

可以看到里面empty字段，字段类型是seL4_SlotRegion，在文档的上方找到了对该字段的说明，该类型是一个C结构体，该结构体包含了两个这指针，即start和end。它标示着初始线程CNode插槽的区域，start指向第一个插槽，而end指向最后一个插槽的下一个位置，因此end-1指向的是这片插槽中的最后一个位置。
在代码中，经常能够看到一些突兀的的量，例如seL4_CapInitThreadCNode,seL4_CapInitThreadTCB，这些东西都没定义，从何而来？

可以是在初始线程的CSpace中包含的，前15个槽（如果没有MSC的是14个槽）包含了如上表指定的特定的能力。
在修改了上述代码之后，再次编译运行可以看到如下的输出：

从main.c中继续寻找TODO：

 // TODO delete the created TCB capabilities

// check first_free_slot is empty
error = seL4_CNode_Move(seL4_CapInitThreadCNode, first_free_slot, seL4_WordBits,
                        seL4_CapInitThreadCNode, first_free_slot, seL4_WordBits);
ZF_LOGF_IF(error != seL4_FailedLookup, "first_free_slot is not empty");

// check last_slot is empty
error = seL4_CNode_Move(seL4_CapInitThreadCNode, last_slot, seL4_WordBits,
                        seL4_CapInitThreadCNode, last_slot, seL4_WordBits);
ZF_LOGF_IF(error != seL4_FailedLookup, "last_slot is not empty");

可以看到，这里要求我们做到是删除创建的能力。

如何删除能力？

上面的代码检查first_free_slot和last_slot是不是空的，结果当然不是空的，因为你复制了TCB能力到这些槽里面去。检查一个能力槽是不是空的方法很巧妙：尝试移动能力槽中的能力到他们自身。如果源槽是空的则该操作应以一个错误码seL4_FailedLookup而结束，如果不是空的则是错误码seL4_DeleteFirst。
有两种可以删除能力的方法：

• 在复制的能力上使用seL4_CNode_Delete删除
• 在原生的能力上使用seL4_CNode_Revoke进行能力回收，回收所有复制的能力

下面查一下这两个方法：

seL4_CPtr 是一个无符号整数类型，表示能力指针（capability pointer），它实际上是能力槽的索引。也就是说，first_free_slot 本身就是一个索引，指向 CSpace 中的某个能力槽。这里的深度指的是传入后进行解析的时候的解析位数，例如传入的index为10101100，那么深度为1的时候就解析一位，即最高位1，当深度4的时候解析前四位，即1010，也就是十进制10，以此类推，所以深度是一个必不可少且非常重要的值，因此first_free_slot是第二个参数。

error = seL4_CNode_Revoke(seL4_CapInitThreadCNode, seL4_CapInitThreadTCB,seL4_WordBits);

//或者使用Delete
error = seL4_CNode_Delete(seL4_CapInitThreadCNode, first_free_slot, seL4_WordBits);
ZF_LOGF_IF(error,"Failed to delete slot");

error = seL4_CNode_Delete(seL4_CapInitThreadCNode, last_slot, seL4_WordBits);
ZF_LOGF_IF(error,"Failed to delete slot");

主要是深度无法确定，在输出的初始化CNode插槽数量的时候可以看到，输出是65536，也就是2的16次方，我以为深度是16，但是传入16不对，错误信息是非法槽，所以应该是深度错了，解析的时候有问题。再看到复制能力的时候，也需要传入深度，程序中传入的深度是seL4_WordBits，将这个值输出后发现是64，是再64位的机器上，所以插槽的索引也是64位的，但是插槽数量只有2¹⁶个，所以就是有多余的用不上的，因此深度应是64，实际有用的只有低16位，但是默认解析是从高位解析的。
输出为：

调用能力

可以看到最后一个TODO是调用能力挂起当前线程，可以使用seL4_TCB_Suspend这个方法尝试挂起当前线程。先查到该方法：

这个简单，代码如下

seL4_TCB_Suspend(seL4_CapInitThreadTCB);

传入的是对线程TCB操作的能力。输出如下：

还有进一步的训练，啥时候想起来再做吧。