当前位置：首页 > news >正文

seL4 Threads（四）

news 来源：原创 2024/9/26 1:21:01

官网链接: Threads

Threads

这篇教程主要是使用seL4中的threads。

TCB Thread Control Blocks

seL4提供了线程代表执行的上下文以及管理处理器时间。seL4中的线程是通过线程控制块对象（TCB）实现的，每个内核线程都有一个线程控制块。
线程控制块包括以下的这些信息：

优先级以及最大控制优先级
寄存器状态以及浮点数上下文
CSpace 能力
VSpace 能力
发送错误信息的端点能力
回复能力槽

调度模式

seL4的调度器选择下一个线程在特定的处理核心上运行，并且该调度器是一个基于优先级的轮转调度器。调度器选择运行的线程状态时runnable，也就是说，可恢复且不会阻止任何的IPC操作。

priorities 优先级

调度器每次选择最高优先级的可运行的线程。seL4提供了0-255的优先级，255是最大优先级（seL4_MinPrio、seL4_MaxPrio）。
TCBs也有一个最大控制优先级（MCP），它作为优先级上的非正式能力控制。

Round robin 轮转调度

当多个线程都可运行且具有相同的优先级的时候，他们的调度是按照先进先出（队列）的方式轮转。更具体的来讲，内核时间以固定时间片（时钟周期）来计算，每个TCB都有一个时间片字段，标识该TCB在被抢占之前可以执行的时钟周期数量。内核定时器驱动程序被配置为触发一个周期性中断来标记每个时钟周期。当时间片耗尽时，轮询调度将被应用。线程可以使用seL4_Yield系统调用放弃其当前时间片。

Domain scheduling 域调度

为了提供保密性，seL4提供了一个顶级的分层调度器，该调度器提供静态的，循环的调度分区（域）调度。域在编译时通过循环调度进行静态配置，并且是不可抢占的，导致域的完全确定性调度。
线程可以被指定域，并且线程只有在他们的域被激活的时候才会被调度。跨域的进程通信（IPC）会被延迟到域切换的时候，且在不同域之间无法使用seL4_Yield系统调用。当一个被调度的域中没有可以运行的线程的时候，一个特定的域闲置线程将会运行知道域切换时。
给一个线程指定域需要seL4_DomainSet能力。该能力允许一个线程可以被添加到任何的域。

seL4_Error seL4_DomainSet_Set(seL4_DomainSet _service, seL4_Uint8 domain, seL4_TCB thread);

Thread Attribute 线程属性

seL4线程是通过调用TCB对象来配置的。

实操 Exercises

这篇教程指导你通过使用TCB调用在相同的地址空间中去创建一个新的线程，并且传递参数给新的线程。此外，你将会了解如何调试一个虚存错误。
这篇教程最后，您希望生成（spawn）一个新线程来调用下面代码示例中的函数。

CapDL loader

之前的教程都是在根任务中进行的，其是由seL4启动协议设置的起始CSpace布局。这篇教程使用capDL loader，是一个分配静态配置的对象和能力的根任务。
capDL loader解析系统的静态描述以及相关的ELF二进制文件。它通常是在Cmakes工程中使用，但是我们在该课程中使用它以减少相关的冗余代码。你构建的程序最终将会以他自己的CSpace和VSpace结束，也就是和根任务是相分离的，这就意味着像seL4_CapInitThreadVSpace 这样的CSlots在被capDL loader加载的程序中没有意义。

CapDL工程相关的信息可以看这个链接

Configure a TCB 配置一个TCB

当第一次构建和运行该教程时，可以看到像下面的输出。额…我也不知道为啥输出的没对齐

Dumping all tcbs! 并且下面的那个表格也是由seL4_DebugDumpScheduler()这个调试系统调用生成的。seL4有一些列的调试系统调用，这些系统调用在调试内核构建中是可用的。
seL4_DebugDumpScheduler()用于输出调度器的当前状态，在系统似乎挂起的情况下，这个函数可以用来调试。
在TCB表格之后，你能看到seL4_Untyped_Retype这个方法由于无效参数而调用失败。该加载器已经被配置如下的能力和符号。

// the root CNode of the current thread
extern seL4_CPtr root_cnode;
// VSpace of the current thread
extern seL4_CPtr root_vspace;
// TCB of the current thread
extern seL4_CPtr root_tcb;
// Untyped object large enough to create a new TCB objectextern seL4_CPtr tcb_untyped;
extern seL4_CPtr buf2_frame_cap;
extern const char buf2_frame[4096];// Empty slot for the new TCB object
extern seL4_CPtr tcb_cap_slot;
// Symbol for the IPC buffer mapping in the VSpace, and capability to the mapping
extern seL4_CPtr tcb_ipc_frame;
extern const char thread_ipc_buff_sym[4096];
// Symbol for the top of a 16 * 4KiB stack mapping, and capability to the mapping
extern const char tcb_stack_base[65536];
static const uintptr_t tcb_stack_top = (const uintptr_t)&tcb_stack_base + sizeof(tcb_stack_base);

练习： 使用上面提供的能力修复如下的seL4_Untyped_Retype 这个调用（下面代码），因此可以在tcb_cap_slot中创建一个新的能力。

int main(int c, char* arbv[]) {printf("Hello, World!\n");seL4_DebugDumpScheduler();// TODO fix the parameters in this invocationseL4_Error result = seL4_Untyped_Retype(seL4_CapNull, seL4_TCBObject, seL4_TCBBits, seL4_CapNull, 0, 0, seL4_CapNull,1)ZF_LOGF_IF(result, "Failed to retype thread: %d", result);seL4_DebugDumpScheduler();

可以看到这个TODO的方法里面有两个seL4_CapNull，这个的意思代表是空能力，用于表示该位置没有有效的能力。这三个seL4_CapNull就是我们需要填充的内容。
根据 Untyped这一章可以确定这三个位置应该分别填写什么，第一个是untyped的能力，第二个是CNode也就是要将新创建的能力放在那个CNode中，可以看到后面两个参数是0，所以是调用寻址，最后一个是要将新创建的能力放在那个CSlot中。结合上面加载器配置好的符号，因此修改代码如下：

seL4_Error result = seL4_Untyped_Retype(tcb_untyped, seL4_TCBObject, seL4_TCBBits, root_cnode, 0, 0, tcb_cap_slot,1)

而也正如教程中所说的一样，一旦TCB被创建，它将会作为’tcb_threads’的孩子显示在seL4_DebugDumpSchedule()的输出中。在整个教程中，你可以使用此系统调用来调试你设置的一些TCB属性，可以看到输出如下。
在这里插入图片描述
可以看到表后输出的另外一个错误，下面我们需要做的是：当前我们有一个TCB对象，然后将其和当前线程配置成一样的CSpace和VSpace。使用我们提供的IPC，但不要设置异常处理器，因为在调试版本中内核将会打印我们收到的任何错误信息。

//TODO fix the parameters in this invocation
result = seL4_TCB_Configure(seL4_CapNull, seL4_CapNull, 0, seL4_CapNull, 0, 0, (seL4_Word) NULL, seL4_CapNull);
ZF_LOGF_IF(result, "Failed to configure thread: %d", result);

先查询一下这个方法的用法。
在这里插入图片描述
因此我们将该代码修改为如下：

result = seL4_TCB_Configure(tcb_cap_slot, //要配置的TCB的能力seL4_CapNull, //设置该线程的故障处理端点（fault endpoint），用于处理异常，也就是异常处理器，不做设置root_cnode, 			  //新的CSpace的根能力seL4_CapNull, //可选参数，与能力空间根相关的权限和配置数据，设置为0则无影响root_vspace, 			  //新的VSpace的根能力0, 			  //x86和ARM处理器中无用(seL4_Word) thread_ipc_buff_sym, //线程IPC缓冲区的虚拟地址，缓冲区不能跨越页边界tcb_ipc_frame//用于映射IPC缓冲区的物理内存帧能力);

可以看到输出，已经到了下一个TODO，现在新创建的线程和当前线程拥有相同的CSpace和VSpace。
在这里插入图片描述

使用seL4_TCB_SetPriority修改优先级

新创建的线程优先级为0，而由loader创建的线程优先级是254，现在我们需要修改我们创建的新线程优先级以便于使其能与当前线程进行循环调度。
使用seL4_TCB_SetPriority设置优先级。要记住一点，想要设置一个线程的优先级，调用线程必须有权这样做（能力）。在这个例子中，主线程能使用他自己的TCB能力，它的MCP（最大控制优先级）为254。
在这里插入图片描述
因此修改代码如下：

// TODO fix the call to set priority using the authority of the current thread
// and change the priority to 254
result = seL4_TCB_SetPriority(tcb_cap_slot, root_tcb, 254);
ZF_LOGF_IF(result, "Failed to set the priority for the new TCB object.\n");
seL4_DebugDumpScheduler();

可以看到输出来到了下一个TODO：
在这里插入图片描述

设置初始寄存器的状态

在设置了该线程的初始寄存器之后，这个TCB差不多就能跑了。你需要将程序计数器和对战指针设置为有效值，否则线程将会立即崩溃。libsel4utils包含一些用于以与平台无关的方式设置寄存器内容的函数。我们可以使用这些方法去设置程序计数器和堆栈指针。注意：假定的是在所有平台中栈是向下增长的。（栈底在高地址部分）
练习：设置新线程去调用函数new_thread。你可以使用调试系统调用以验证你是否正确设置了IP（instruction pointer）。
先看一眼代码：

seL4_UserContext regs = {0};
int error = seL4_TCB_ReadRegisters(tcb_cap_slot, 0, 0, sizeof(regs)/sizeof(seL4_Word), &regs);
ZF_LOGF_IFERR(error, "Failed to read the new thread's register set.\n");// TODO use valid instruction pointer
sel4utils_set_instruction_pointer(&regs, (seL4_Word)NULL);
// TODO use valid stack pointer
sel4utils_set_stack_pointer(&regs, NULL);
// TODO fix parameters to this invocation
error = seL4_TCB_WriteRegisters(seL4_CapNull, 0, 0, 0, &regs);
ZF_LOGF_IFERR(error, "Failed to write the new thread's register set.\n""\tDid you write the correct number of registers? See arg4.\n");
seL4_DebugDumpScheduler();

在这里插入图片描述
可以看到seL4_TCB_ReadRegisters方法的作用是将寄存器中的内容读到regs中。它有五个参数：

tcb_cap_slot：要读取寄存器的线程的 TCB 能力。
是否要挂起源线程
体系结构相关
要读取的寄存器数目
指向 seL4_UserContext 结构的指针，用于存储读取的寄存器值
再看看libsel4utils提供的的两个方法：

需要提一下：

// Symbol for the top of a 16 * 4KiB stack mapping, and capability to the mapping
extern const char tcb_stack_base[65536];
// 这个是基地址加上整个数组大小，指向了整个数组的高地址部分作为栈顶，整个栈向下增长，入栈地址减，出栈地址增
static const uintptr_t tcb_stack_top = (const uintptr_t)&tcb_stack_base + sizeof(tcb_stack_base);

因此这部分代码如下：

seL4_UserContext regs = {0};
int error = seL4_TCB_ReadRegisters(tcb_cap_slot, 0, 0, sizeof(regs)/sizeof(seL4_Word), &regs);
ZF_LOGF_IFERR(error, "Failed to read the new thread's register set.\n");// TODO use valid instruction pointer
sel4utils_set_instruction_pointer(&regs, (seL4_Word)&new_thread);
// TODO use valid stack pointer
sel4utils_set_stack_pointer(&regs, tcb_stack_top);
// TODO fix parameters to this invocation
error = seL4_TCB_WriteRegisters(tcb_cap_slot, 0, 0, sizeof(regs)/sizeof(seL4_Word), &regs);
ZF_LOGF_IFERR(error, "Failed to write the new thread's register set.\n""\tDid you write the correct number of registers? See arg4.\n");
seL4_DebugDumpScheduler();

再次执行之后可以看到：
在这里插入图片描述

开启线程

现在可以启动线程了，使TCB变成runnable且能够被seL4调度器调度。可以通过改变seL4_TCB_WriteRegisters的第二个参数为1且删除掉seL4_TCB_Resume调用做到，也可以通过修改下面的resume调用做到。
修改代码为：

// TODO resume the new thread
error = seL4_TCB_Resume(tcb_cap_slot);
ZF_LOGF_IFERR(error, "Failed to start new thread.\n");

可以看到输出为：
在这里插入图片描述
后面还跟了一个错误，这个错误的格式说明在上一节中说过。

传递参数

通过上面的输出可以看到传递给新线程的参数都是0。你可以通过使用辅助函数sel4utils_arch_init_local_context设置参数或者通过直接操作你体系结构下的目标寄存器来传递参数。
练习：更新使用seL4_TCB_WriteRegisters写入的值，以分别将值1、2、3作为arg1、arg2和arg3传递。修改代码如下：

seL4_UserContext regs = {0};
int error = seL4_TCB_ReadRegisters(tcb_cap_slot, 0, 0, sizeof(regs)/sizeof(seL4_Word), &regs);
ZF_LOGF_IFERR(error, "Failed to read the new thread's register set.\n");// TODO use valid instruction pointer
//sel4utils_set_instruction_pointer(&regs, (seL4_Word)&new_thread);
// TODO use valid stack pointer
//sel4utils_set_stack_pointer(&regs, tcb_stack_top);
// passing arguments
sel4utils_arch_init_local_context((void *)new_thread,(void *)1, (void *)2, (void *)3,(void *)tcb_stack_top,&regs);
// TODO fix parameters to this invocation
error = seL4_TCB_WriteRegisters(tcb_cap_slot, 0, 0, sizeof(regs)/sizeof(seL4_Word), &regs);
ZF_LOGF_IFERR(error, "Failed to write the new thread's register set.\n""\tDid you write the correct number of registers? See arg4.\n");
seL4_DebugDumpScheduler();

需要将之前的设置IP和stack的代码注释掉，使用这一个参数可以全部设置掉。输入如下
在这里插入图片描述

解决故障

现在你已经创建并且配置了一个新的线程，并且给了它初始的参数。这个教程的最后一部分是当你的线程出错的时候你应该怎么办。之后有进一步的详细的错误处理教程（官网说的，不是我说的）。现在的话，我们可以依靠内核打印错误信息，因为我们创建的线程没有错误处理程序。
在上面图片的输出中，我们可以看到一个能力错误。错误的第一部分是内核不能发送一个错误给错误处理器，因为没设置这玩意。然后内核就输出了它尝试发送的错误信息。在这个案例中，该错误是虚存错误。新线程尝试访问地址0x2地方的数据，这是一个非法的未映射的地址。输出显示故障时线程的程序计数器为0x401e6c（这条指令出错）。
故障状态寄存器也会输出，可以通过相关架构手册进行解码。此外，内核会从当前栈指针打印原始栈转储。栈转储的大小是可配置的，使用 KernelUserStackTraceLength CMake 变量进行设置。
要调查故障，您可以使用如 objdump 这样的工具来检查导致故障的 ELF 文件中的指令。在这种情况下，ELF 文件位于 ./<BUILD_DIR>/<TUTORIAL_BUILD_DIR>/threads。

这一块我本想操作一下，但是elf文件找了半天，错误信息看起来十分费劲。但教程下面给出了修改的方法：

确保 arg2 拥有一个有效的地址，而不是直接传入立即数，因为在new_thread方法中有一行代码func(*(int *)arg2);，这表明了arg2必须是一个指向int的指针，且这行代码实际上是调用了arg1所指向的函数，将arg2中存储的整数值作为参数传入，因此如果传入的是一个立即数的话，会把传入的立即数当作地址操作里面的数，这是非法的。
void (*func)(int) = arg1;这行代码说明arg1需要是一个函数指针。

因此代码如下：

// 全局参数
int a2 = 10;// 自定义函数
void my_function(int arg) {// 输出 arg 的值，例如使用 printfprintf("Argument: %d\n", arg);
}
sel4utils_arch_init_local_context((void *)new_thread,(void *)my_function, (void *)&a2, (void *)3, //传入a2的地址作为第二个参数(void *)tcb_stack_top,&regs);