sel4 线程和执行

线程

seL4提供了表示执行上下文和管理处理器时间的线程。在seL4中，线程由其线程控制块对象(TCB)表示。每个TCB都有一个相关的CSpace(见第3章)和VSpace(见第7章)，它们可以被其他线程共享。TCB还可以有一个IPC缓冲区(见第4章)，用于在IPC或内核对象调用期间传递不适合体系结构定义的消息寄存器的额外参数。虽然一个线程不需要有IPC缓冲区，但是它不能执行大多数内核调用，因为它们需要cap传输。每个线程只属于一个安全域(见6.3节)。

线程创建

与其他对象一样，tcb是使用seL4无类型Retype()方法创建的(请参阅

2.4节)。新创建的线程最初是不活动的。通过使用seL4 TCB SetSpace()或seL4 TCB Configure() methods设置它的CSpace和VSpace，然后使用初始堆栈指针和指令指针调用seL4 TCB WriteRegisters()来配置它。然后，可以通过将seL4 TCB WriteRegisters()调用中的Resume -target参数设置为true或单独调用seL4 TCB Resume()方法来激活线程。在多核机器中，线程将运行在最初创建TCB的同一CPU上。但是，可以通过调用seL4 TCB SetAffinity()将其迁移到其他cpu上。

线程失活

seL4 TCB Suspend()方法取消激活一个线程。挂起的线程稍后可以被恢复。它们的挂起状态可以通过seL4 TCB ReadRegisters()和seL4 TCB CopyRegisters()方法检索。如果不需要，它们也可以重新配置和重用，或者无限期地挂起。线程将在其TCB的最后一个功能被删除时自动挂起。

调度

seL4使用具有256个优先级级别的抢占式轮询调度器。所有线程都有一个最大控制优先级(MCP)和一个优先级，后者是线程的有效优先级。当一个线程创建或修改一个线程(包括它自己)时，它只能设置另一个线程的优先级和MCP小于或等于它自己的MCP。线程优先级和MCP可以用seL4 TCB Configure()和seL4 TCB SetPriority()， seL4 TCB SetMCPriority()方法设置。

异常

每个线程都有一个相关联的异常处理程序端点。如果线程导致

异常时，内核会创建一个带有相关细节的IPC消息并将其发送给端点。然后，该线程可以采取适当的操作。故障IPC消息参见6.2。

为了启用异常处理程序，异常处理程序端点的功能必须存在于生成异常的线程的CSpace中。可以使用seL4 TCB SetSpace()或seL4 TCB Configure()方法设置异常处理程序端点。通过这些方法，可以将异常处理程序的功能地址与线程相关联。当生成异常时使用此地址查找处理程序端点。但是请注意，这些方法不会检查线程的CSpace中的指定地址上是否存在端点功能。只有在实际发生异常时才会查找该功能，如果查找失败，则不会发送异常消息，线程将无限期地挂起。

异常端点必须具有发送和授予权限。回复异常消息重启线程。对于某些异常类型，应答的内容消息可以用来设置正在重新启动的线程的寄存器中的值。详见6.2节。

读/写寄存器方法的消息布局

可以使用seL4 TCB ReadRegisters()和seL4 TCB writereregisters()方法读写线程的寄存器。对于一些寄存器,内核将默默地掩盖某些位或范围的位,并强迫他们包含特定的值,以确保他们不能恶意设置为值会妥协运行系统,或尊重的价值观体系结构规范规定为一定值。在X86上，这些位目前是:

寄存器内容通过IPC缓冲区传送。下面给出了寄存器被复制到/复制到的IPC缓冲区位置。

缺点

线程的操作可能会导致错误。错误被传递给线程的exception处理程序，以便它可以采取适当的操作。故障类型在消息标签中指定，包括:seL4 fault CapFault、seL4 fault VMFault、seL4 fault UnknownSyscall、seL4 fault UserException、seL4 fault DebugException、seL4 fault NullFault(表示没有发生故障，正常IPC message)。

错误以模仿来自错误线程的调用的方式传递。这意味着要发送错误消息，错误端点必须同时具有写权限和授予权限。

capability 缺陷

能力故障可能发生在两个地方。首先，当seL4 Call()或seL4 Send()系统调用引用的功能查找失败(seL4 NBSend()对无效功能的调用静默失败)。在这种情况下，发生故障的能力可能是正在调用的能力，或者IPC缓冲区中caps字段中传递的额外能力。

其次，当seL4 Recv()或seL4 NBRecv()对不存在、不是端点或通知功能或没有接收权限的功能调用时，可能会发生功能故障。

响应错误IPC将重新启动出错的线程。IPC消息的内容见表6.1。

未知的系统调用

当线程以seL4未知的系统调用号执行系统调用时，就会发生此错误。发生故障的线程的注册集被传递给线程的异常处理程序，这样，如果一个线程正在被虚拟化，它就可以模拟系统调用。

响应错误IPC允许重新启动线程和/或修改线程的寄存器。如果应答的标签为0，线程将重新启动。另外，如果消息长度不为零，则故障线程的寄存器集将被更新，如表6.2和表6.3所示。在这种情况下，更新的寄存器数量由消息标记的length字段控制。

用户异常

用户异常用于交付体系结构定义的异常。例如，如果用户线程试图将一个数字除以0，就会发生这样的异常。

响应错误IPC允许重新启动线程和/或修改线程的寄存器。如果应答的标签为0，线程将重新启动。另外，如果消息长度非零，那么发生故障的线程的寄存器集将被更新，如表6.4和表6.5所示。在这种情况下，更新的寄存器数量由消息标记的length字段控制。

调试异常:断点和观察点

调试异常用于将跟踪和调试相关事件传递给线程。断点点、观察点、跟踪事件和指令性能采样事件都是例子。当内核被配置为包含这些事件时(当配置硬件调试API被设置时)，用户空间线程就支持这些事件。关于可用的硬件调试资源的信息以下列常量的形式呈现:

**seL4 NumHWBreakpoints 😗*定义了硬件平台上所有可用类型的可用硬件中断寄存器的总数。以ARM Cortex A7为例，有6个专用指令断点寄存器和4个专用数据观察点寄存器，总共有10个监视器寄存器。因此，在这个平台上，seL4NumHWBreakpoints被定义为10。指令断点寄存器将始终被分配为较低的api - id，数据观察点将始终跟随它们被分配。

此外，为每个目标平台定义了seL4 NumExclusiveBreakpoints、seL4 NumExclusiveWatchpoints和seL4 NumDualFunctionMonitors，以反映某种类型的可用硬件断点/观察点的数量。

seL4 NumExclusiveBreakpoints：定义仅在指令执行时才可能产生错误的硬件寄存器的数量。目前这只会在ARM平台上设置。第一个独占断点的API-ID在seL4 FirstBreakpoint中给出。如果没有指令中断独占寄存器，则seL4 NumExclusiveBreakpoints将被设置为0,seL4 FirstBreakpoint将被设置为-1。

**seL4 NumExclusiveWatchpoints：**定义仅在数据访问时才可产生故障的硬件寄存器的数量ca。目前这只会在ARM平台上设置。第一个独占观察点的API-ID在seL4 FirstWatchpoint中给出。如果没有数据中断独占寄存器，则seL4 NumExclusiveWatchpoints将被设置为0,seL4 FirstWatchpoint将被设置为-1。

seL4 NumDualFunctionMonitors：定义硬件寄存器的数量，可以在任何类型的访问上产生错误，也就是说，寄存器同时支持指令和数据中断。目前只在x86平台上设置。第一个双功能监视器的API-ID在seL4 FirstDualFunctionMonitor中给出。如果没有双函数中断寄存器，seL4 NumDualFunctionMonitors将被设置为0,seL4 FirstDualFunctionMonitor将被设置为-1。

调试异常:单步

当配置了用户空间线程时(当设置了配置硬件调试API时)，内核提供了对使用硬件单步用户空间线程的支持。为此，它公开调用，seL4 TCB configuresinglestep。

调用者需要选择一个API-ID，该API-ID对应于指令断点点，用于设置单步执行功能(例如，API-ID从0到seL4 NumExclusiveBreakpoints - 1)。然而，并不是所有的硬件平台都需要一个实际的硬件断点寄存器来提供单步功能。如果调用者的硬件平台需要使用硬件断点寄存器，它将使用bp num中给它的断点寄存器，并在bp_was_consumed中返回true。如果底层平台不需要硬件断点来提供单个步进，那么seL4将在bp was consume中返回false，并保持bp num不变。

如果bp_was_consumed是真的,调用者不应试图重新配置bp num断点或监视点使用直到调用者禁用单步和注册发布,随后通过调用seL4 TCB ConfigureSingleStepping,或与n instr fault-reply 0。将num指令设置为0将禁用单步执行。

在需要为单个步进功能配置实际硬件寄存器的架构上，seL4将限制可以配置为单步进的寄存器的数量，在任何给定时间为一个。当前为单步调试配置的寄存器(如果有的话)将是单步调试故障应答中的隐式bp num参数。

内核的单步操作，也支持在传递单步错误消息之前跳过一定数量的指令。在单步执行时，应该将Num指令设置为1，或者在恢复单步执行之前将任何非零整数值设置为跳过这么多指令。还可以在单步调试故障的故障应答中设置这个跳过计数。

VM异常

该线程导致页面错误。响应错误IPC将重新启动线程。IPC消息的内容如下。

域

用域来隔离独立的子系统，使它们之间的信息流限制在之间。内核根据一个固定的、由时间触发的时间表在域之间切换。固定的调度通过常量CONFIG-NUM_DOMAINS和全局变量ksDomSchedule编译到内核中。

线程只属于一个域，并且只在该域处于活动状态时运行。seL4 DomainSet Set()方法更改线程的域。调用者必须拥有域权能和线程的TCB权能。初始线程以域权能开始(见4.1节)。