版本 13.0.0

seL4 Foundation https://sel4.systems

2024 年 7 月 1 日

本文是 seL4 Reference Manual v13.0.0 的中文翻译， 原文版权所有 © the seL4 authors and contributors。 根据 GPL-2.0-only 许可证发布，本译文同样遵循 GPL-2.0 许可。 seL4® 是 LF Projects, LLC 的商标。

致谢

本文档的主要作者是 Matthew Grosvenor 和 Adam Walker，贡献者包括 Adrian Danis、Andrew Boyton、Anna Lyons、Axel Heider、Branden Robinson、David Greenaway、Etienne Le Sueur、Gernot Heiser、Gerwin Klein、Godfrey van der Linden、Jimmy Brush、Kevin Elphinstone、Matthew Fernandez、Matthias Daum、Michael von Tessin、Nick Spinale、Peter Chubb、Simon Winwood、Thomas Sewell、Timothy Bourke 和 Toby Murray。

作者和贡献者可以通过 seL4 开发者邮件列表或 seL4 Discourse 论坛联系。详情请参阅 https://sel4.systems/contact/。

第 1 章 引言

seL4 微内核（microkernel）是一个操作系统内核，旨在为各种应用领域的系统提供安全、可靠和可信的基础。作为微内核，它提供了少量可用于构建应用程序的机制，如虚拟地址空间、线程和进程间通信（IPC）。

少量的机制意味着较小的实现规模——根据架构和配置的功能不同，大约为 10,000 行 C 代码。这使得在 Isabelle/HOL 定理证明器中对内核进行了形式化验证 [Boyton, 2009¹, Cock et al., 2008², Derrin et al., 2006³, Elkaduwe et al., 2008⁴, Klein et al., 2009⁵, Tuch et al., 2007⁶, Winwood et al., 2009⁷]，进而能够证明内核对完整性 [Sewell et al., 2011⁸] 和机密性 [Murray et al., 2013⁹] 的强制执行。内核的小规模也对完成最坏情况执行时间的完整且健全的分析起到了关键作用 [Blackham et al., 2011¹⁰, 2012¹¹]。[Klein et al. 2014¹²] 对验证进行了全面的技术总结，seL4 白皮书 [Heiser, 2020¹³] 则提供了一个更简短但更易懂的概述。

内核的功能正确性证明已在多种架构和平台上可用。对于 Arm32，可选地包括虚拟机管理器扩展，以及上述安全证明。有关当前支持的证明，请参阅 seL4 文档站点 [seL4 Authors, 2021a¹⁴]。

本手册从用户角度描述 seL4 内核的 API。文档首先简要概述 seL4 微内核设计，然后介绍 seL4 内核向用户空间公开的高级 API。

虽然我们已尽力确保本手册准确反映 seL4 内核的行为，但本文档绝非内核的形式化规范。当需要了解内核在特定情况下的精确行为时，用户应参考 seL4 的抽象规范 [seL4 Authors, 2021b¹⁵]，其中给出了完全形式化的描述。

第 2 章 内核服务与对象

微内核提供有限数量的服务原语；更复杂的服务可以基于这些原语作为应用程序来实现。这样，系统的功能可以在不增加特权模式下的代码和复杂性的情况下得到扩展，同时仍然可以为各种应用领域支持大量潜在的服务。

请注意，某些服务仅在内核配置为支持 MCS（mixed-criticality system，混合关键性系统）时才可用。

seL4 提供的基本服务如下：

• 线程 是 CPU 执行的抽象，支持软件运行；
• 调度上下文（仅 MCS）是 CPU 执行时间的抽象；
• 地址空间 是虚拟内存空间，每个空间包含一个应用程序。应用程序只能访问其地址空间内的内存；
• 通过端点进行进程间通信（IPC）允许线程使用消息传递进行通信；
• 回复对象（仅 MCS）用于存储一次性回复权能，在消息传递过程中由接收方提供；
• 通知（Notification）提供类似于二进制信号量的非阻塞信号机制；
• 设备原语允许将设备驱动程序实现为非特权应用程序。内核通过 IPC 消息导出硬件设备中断；
• 权能空间（CSpace）存储对内核服务的权能（即访问权限）及其簿记信息。

本章概述了这些服务，并描述了用户空间应用程序如何访问内核对象以及如何创建新对象。

2.1 基于权能的访问控制

seL4 微内核提供基于权能（capability）的访问控制模型。访问控制管理所有内核服务；为了执行操作，应用程序必须调用其拥有的、具有请求服务所需足够访问权限的权能。通过这种方式，系统可以配置为将软件组件相互隔离，并通过选择性地授予特定通信权能来启用经过授权的、受控的组件间通信。这实现了具有高度保证的软件组件隔离，因为只允许显式通过权能持有而授权的操作。

权能（capability）是一个不可伪造的令牌，引用特定的内核对象（如线程控制块），并携带控制可调用哪些方法的访问权限。概念上，权能驻留在应用程序的权能空间中；该空间中的一个地址指向一个槽位，该槽位可能包含也可能不包含权能。应用程序可以使用持有该权能的槽位地址来引用权能——例如请求内核服务。这意味着，seL4 权能模型是隔离式（或分区式）权能系统的一个实例，其中权能由内核管理。

权能空间实现为由内核管理的权能节点（CNode）组成的有向图。CNode 是一个槽位表，其中每个槽位可以包含进一步的 CNode 权能。权能空间中权能的地址是构成目标槽位路径的 CNode 内槽位索引的拼接。我们将在第 3 章详细讨论 CNode 对象。

权能可以在权能空间内复制和移动，也可以通过 IPC 发送。这允许创建具有特定访问权限的应用程序、将权限委托给另一个应用程序，以及向应用程序授予对新创建（或选定）内核服务的权限。此外，权能可以被铸造（mint）以创建具有原始权能权限子集的派生权能（永远不会有更多权限）。新铸造的权能可用于部分权限委托。

权能也可以被撤销（revoke）以收回权限。撤销会递归地移除从被撤销的原始权能派生的所有权能。权能通过系统的传播由基于 take-grant 的模型控制 [Elkaduwe et al., 2008⁴, Boyton, 2009¹]。

2.2 系统调用

seL4 内核为线程间通信提供消息传递服务。此机制也用于与内核提供的服务进行通信。存在标准的消息格式，每条消息包含若干数据字，可能还包含一些权能。这些消息的结构和编码在第 4 章中有详细描述。

线程通过调用其权能空间中的权能来发送消息。当以这种方式调用端点、通知或回复权能时，消息将通过内核传输到另一个线程。当调用其他内核对象的权能时，消息将被解释为特定于内核对象类型的方法调用。例如，使用格式正确的消息调用线程控制块（TCB）权能将暂停目标线程。

从根本上说，我们可以将内核视为提供三个系统调用（system call）：Send（发送）、Receive（接收）和 Yield（让出）。但是，基本 Send 和 Receive 调用也有组合和变体。一个重要的变体是 Call 操作，它由标准的 Send 操作原子地后跟一个等待 Reply 的 Receive 变体组成。回复消息总是通过特殊资源传递，而不是使用标准 IPC 机制；详见下文的 seL4_Call()。

调用端点和通知以外的内核对象的方法使用 Send 或 Call，取决于调用者是否希望从内核获得回复（Call）或不希望（Send）。通过使用 libsel4 API 提供的函数，您始终可以保证使用更合适的一个。Yield 系统调用不与任何内核对象关联，是唯一不调用权能的操作。在 MCS 配置中，Wait 是 Receive 的一个变体，不需要提供回复对象——在非 MCS 配置中，Wait 与 Receive 是同义的，因为两者都不接受回复对象。

基本系统调用如下：

• seL4_Yield() 是唯一不需要使用权能的系统调用。它放弃调用线程剩余的时间片，并触发内核的调度器。如果没有其他与调用者相同优先级的可运行线程，调用线程将立即以新的时间片重新调度。在 MCS 配置中，此行为取决于调度上下文的状态；见第 6.1.7 节。

• seL4_Send() 通过指定的权能传递消息。如果调用的权能是端点，并且没有接收者准备好立即接收消息，发送线程将阻塞直到消息可以传递。接收对象不会返回错误代码或响应。

• seL4_Recv()（“receive”）由线程用于通过端点或通知接收消息。如果没有发送者或通知等待，调用者将阻塞直到消息或通知可以传递。此系统调用仅适用于 Endpoint 或 Notification 权能，对其他权能类型尝试时会触发故障（见第 6.2 节）。在 MCS 配置中，Receive 接受一个回复权能——对回复对象的权能——作为参数。

以下系统调用是 seL4_Send() 和 seL4_Recv() 的变体和组合，用于高效地适应系统编程中的常见用例：

• seL4_NBSend() 对端点执行轮询发送。如果消息不能立即传递，即目标 Endpoint 上没有接收者等待，消息将被静默丢弃。发送线程继续执行。与 seL4_Send() 一样，不会返回错误代码或响应。

• seL4_NBRecv() 由线程用于检查通知对象上待处理信号或端点上待处理消息，而不会阻塞。此系统调用仅适用于端点和通知对象权能，对其他权能类型尝试时会触发故障（见第 6.2 节）。

• seL4_Call() 结合了 seL4_Send() 和 seL4_Recv()，但有一些重要区别。该调用会阻塞发送线程，直到其消息被传递并收到回复消息。

  当调用内核服务（端点以外）的权能时，使用 seL4_Call() 允许内核通过回复消息返回错误代码或其他响应。当发送的消息通过 Endpoint 传递到另一个线程时，内核执行与 seL4_Send() 相同的操作。接下来发生的情况取决于内核配置。对于 MCS 配置，内核随后更新接收方提供的回复对象。回复对象是用于跟踪回复消息的容器，用于发送回复消息并唤醒调用者。在非 MCS 配置中，内核随后将一个特殊的回复权能存放在接收方 TCB 的专用槽位中。该回复权能是发送回复消息并唤醒调用者的一次性权限，意味着内核在调用后立即使其失效。对于两种变体，调用线程都被阻塞，直到对回复对象的权能被调用。更多信息见第 4.2.4 节。

• seL4_Reply() 用于响应 seL4_Call()，通过调用由 seL4_Call() 系统调用生成并存储在回复线程 TCB 专用槽位中的回复权能。它的行为与使用 seL4_Send() 调用回复权能完全相同，如第 4.2.4 节所述。

• seL4_ReplyRecv() 结合了 seL4_Reply() 和 seL4_Recv()。它的存在主要是出于效率考虑，即回复请求并等待下一个的常见情况可以在单个内核系统调用中完成，而不是两个。从回复到接收阶段的转换也是原子的。

• seL4_Wait() 的工作方式类似 seL4_Recv()；在非 MCS 配置中，它们实际上是同义的。在 MCS 配置中，seL4_Wait() 用于不期望回复的情况。与 seL4_Recv() 不同，seL4_Wait() 不接受回复权能。

• seL4_NBWait()（仅 MCS）由线程用于轮询通过端点或通知的消息。如果没有发送者或通知待处理，系统调用立即返回。

• seL4_NBSendWait()（仅 MCS）将 seL4_NBSend() 和 seL4_Wait() 组合成一个原子系统调用。

• seL4_NBSendRecv()（仅 MCS）将 seL4_NBSend() 和 seL4_Recv() 组合成一个原子系统调用。

2.3 内核对象

本节简要概述可由应用程序调用的内核实现的对象类型及其实例（也简称为对象）。这些对象的接口构成了内核本身的接口。内核服务的创建和使用是通过这些内核对象的创建、操作和组合来实现的：

• CNode（见第 3 章）存储权能，赋予线程调用特定对象方法的权限。每个 CNode 有固定数量的槽位，始终是 2 的幂，在 CNode 创建时确定。槽位可以为空或包含权能。

• 线程控制块（TCB；见第 6 章）表示 seL4 中的一个执行线程。线程是根据应用程序与其他线程的交互而被调度、阻塞、解除阻塞等的执行单元。

• 调度上下文（仅 MCS）（SchedContexts；见第 6 章）表示 seL4 中的 CPU 时间。用户可以从无类型对象创建调度上下文，但创建时调度上下文为空，不代表任何时间。最初，每个节点都有一个对 SchedControl 的权能，允许用参数填充调度上下文，结合优先级控制线程对 CPU 时间的访问。

• 端点（Endpoint）（见第 4 章）促进线程间的消息传递通信。IPC 是同步的：尝试在端点上发送或接收的线程将阻塞，直到消息可以传递。这意味着消息传递仅在发送者和接收者在端点处汇合时发生，内核可以通过单次复制传递消息（对于仅使用寄存器的短消息则无需复制）。对端点的权能可以限制为仅发送或仅接收。此外，端点权能可以具有 grant 权限，允许在消息中发送权能。

• 回复对象（仅 MCS）（见第 4 章）跟踪调度上下文捐赠，并提供一次性回复权能的容器。它们由 seL4_Recv() 提供。

• 通知对象（Notification Object）（见第 5 章）提供简单的信号机制。通知是一个字大小的标志数组，每个标志的行为类似于二进制信号量。操作包括在单个操作中发出部分标志的信号、轮询检查任何标志、以及阻塞直到任何标志被发出信号。通知权能可以是仅信号或仅等待。

• 虚拟地址空间对象（见第 7 章）用于为一个或多个线程构建虚拟地址空间（VSpace）。这些对象在很大程度上直接对应硬件的对象，因此是架构相关的。内核还包括用于跟踪地址空间状态的 ASID Pool 和 ASID Control 对象。

• 中断对象（见第 8 章）赋予应用程序接收和确认硬件设备中断的能力。最初，存在一个对 IRQControl 的权能，允许创建 IRQHandler 权能。IRQHandler 权能允许管理与特定设备关联的特定中断源。它被委托给设备驱动程序以访问中断源。IRQHandler 对象允许线程等待和确认各个中断。

• 无类型内存（Untyped Memory）（见第 2.4 节）是 seL4 内核中内存分配的基础。无类型内存权能具有一个方法，允许创建新的内核对象。如果方法成功，调用线程获得对新创建对象的权能。此外，无类型内存对象可以被划分为一组较小的无类型内存对象，允许委托部分（或全部）系统内存。我们将在以下各节中讨论内存管理。

2.4 内核内存分配

seL4 微内核不会为内核对象动态分配内存。相反，必须通过无类型内存权能从应用程序控制的内存区域显式创建对象。应用程序必须对内存拥有显式权限（通过这些无类型内存权能）才能创建新对象，并且所有对象一旦创建就消耗固定量的内存。这些机制可用于精确控制应用程序可用的特定物理内存量，包括能够强制执行应用程序之间或应用程序与设备之间的物理内存访问隔离。除了硬件规定的限制外，内核中没有任意的资源限制，因此避免了通过资源耗尽进行的许多拒绝服务攻击。

在启动时，seL4 预分配内核本身所需的内存，包括代码、数据和栈段（seL4 是单内核栈操作系统）。然后创建一个初始用户线程（具有适当的地址和权能空间）。内核随后将所有剩余内存以无类型内存权能的形式交给初始线程，以及一些引导初始线程所需的内核对象的额外权能。这些无类型内存区域随后可以使用 seL4_Untyped_Retype() 方法分割为更小的区域或其他内核对象；创建的对象称为原始无类型内存对象的子对象。

使用 seL4_Untyped_Retype() 创建对象的用户级应用程序获得对生成对象的完全权限。然后可以将其拥有的对该对象的全部或部分权限委托给其一个或多个客户端。

无类型内存对象代表两种不同类型的内存：通用内存或设备内存。通用内存可以被重类型化为任何其他对象类型，并用于内核提供的无类型内存上的任何操作。设备内存涵盖硬件平台确定的为设备保留的内存区域，内核通过以下方式限制这些对象的使用：

• 设备无类型对象只能被重类型化为帧或其他无类型对象；例如，开发者不能从设备内存创建端点。

• 从设备无类型对象重类型化的帧对象不能被设置为线程 IPC 缓冲区，也不能用于创建 ASID 池。

子无类型对象的类型属性（无论是通用内存还是设备内存）继承自其父无类型对象。也就是说，设备无类型对象的任何子对象也将是设备无类型对象。开发者无法更改无类型对象的类型属性。

2.4.1 内存重用

到目前为止描述的模型足以让应用程序分配内核对象、在客户端应用程序之间分配权限，以及获得这些对象提供的各种内核服务。仅此就足以满足简单的静态系统配置。

seL4 内核还允许无类型内存区域被重用。只有当该内存中对象的所有悬空引用（即权能）都已被清除时，才允许重用内存区域。内核跟踪权能派生，即通过 seL4_Untyped_Retype()、seL4_CNode_Mint()、seL4_CNode_Copy() 和 seL4_CNode_Mutate() 方法生成的子对象。由此生成的树结构称为权能派生树（CDT）。例如，当用户通过重类型化无类型内存创建新内核对象时，新创建的权能将作为无类型内存权能的子对象插入 CDT。

对于每个指向无类型内存区域的无类型权能，内核维护一个水位标记，记录该区域先前已分配了多少。每当用户请求内核在无类型内存区域中创建新对象时，内核将执行以下两种操作之一：如果区域中已有已分配的对象，内核将在当前水位标记处分配新对象，并增加水位标记。如果对该区域中先前分配对象的所有权能都已被删除，内核将重置水位标记并从区域开头重新分配新对象。

最后，CNode 对象提供的 seL4_CNode_Revoke() 方法删除从参数权能派生的所有权能。撤销对内核对象的最后一个权能会触发对该现在未被引用对象的销毁操作。这将清理它与其它对象和内核之间所有剩余的内核内依赖关系。此时它不一定会清零与对象关联的所有内存状态。当所有子权能被撤销后，作为第一次重类型化操作的一部分，无类型权能被重置时，整个区域的内存清零将会发生。

要重用内存区域，用户代码可以对原始无类型权能调用 seL4_CNode_Revoke()，从而删除该权能的所有子对象。调用后，对无类型区域内任何对象不再有引用，该区域可以被安全地重新重类型化。

2.4.2 对象大小汇总

在重类型化无类型内存时，了解对象将需要多少内存是很有用的。对象大小在 libsel4 中定义。

请注意，CNode、SchedContext（仅 MCS）和无类型对象具有可变大小。将无类型内存重类型化为 CNode 或 SchedContext，或将无类型对象分割为更小的无类型对象时，seL4_Untyped_Retype() 的 size_bits 参数用于指定生成对象的大小。对于所有其他对象类型，大小是固定的，seL4_Untyped_Retype() 的 size_bits 参数被忽略。

表 2.1：可变大小对象类型的 size_bits 含义

对 seL4_Untyped_Retype() 的单次调用可以将一个无类型对象重类型化为多个对象。要创建的对象数量由其 num_objects 参数指定。所有创建的对象必须是相同类型，由 type 参数指定。在可变大小对象的情况下，每个对象也必须是相同大小。如果所需内存区域的大小（由对象大小乘以 num_objects 计算）大于无类型对象的剩余未分配内存，将导致错误。

以下是创建 SchedContext 对象的有用常量：

• seL4_MinSchedContextBits：调度上下文的最小 log2 大小
• seL4_CoreSchedContextBytes：调度上下文的字节大小（不包括额外补充）
• seL4_RefillSizeBytes：单个额外补充的字节大小

第 3 章 权能空间

回顾第 2.1 节，seL4 实现基于权能的访问控制模型。每个用户空间线程有一个关联的权能空间（CSpace），包含该线程拥有的权能，从而控制线程可以访问的资源。

回顾权能驻留在称为 CNode 的内核管理对象中。CNode 是一个槽位表，每个槽位可以包含权能。这可以包括指向更多 CNode 的权能，形成有向图。概念上，线程的 CSpace 是从其 CSpace 根的 CNode 权能开始可到达的有向图部分。

CSpace 地址指向单个槽位（在 CSpace 中的某个 CNode 中），该槽位可能包含也可能不包含权能。线程使用持有相关权能的槽位地址引用其 CSpace 中的权能（例如在发出系统调用时）。CSpace 中的地址是构成目标槽位路径的 CNode 权能索引的拼接；我们将在第 3.3 节进一步讨论这一点。

回顾权能可以在 CSpace 内复制和移动，也可以在消息中发送（消息发送将在第 4.2.2 节详细描述）。此外，可以从现有权能以更少的权限铸造新权能。回顾第 2.4.1 节，seL4 维护一个权能派生树（CDT），在其中跟踪这些复制的权能与原始权能之间的关系。撤销方法移除所有从选定权能派生的权能（在所有 CSpace 中）。此机制可被服务器用于恢复对已向客户端提供的对象的唯一权限，或被无类型内存管理器用于销毁该内存中的对象以便可以重新重类型化。

seL4 要求程序员从用户空间管理所有内核内数据结构，包括 CSpace。这意味着用户空间程序员负责构建 CSpace 以及在其中对权能进行寻址。本章首先讨论权能和 CSpace 管理，然后讨论权能在 CSpace 中如何被寻址，即应用程序在调用方法时如何引用其 CSpace 中的各个权能。

3.1 权能与 CSpace 管理

3.1.1 CSpace 创建

CSpace 通过创建和操作 CNode 对象来创建。创建 CNode 时，用户必须指定其槽位数，这决定了它将使用的内存量。每个槽位需要 2^seL4_SlotBits 字节的物理内存，并有容量恰好容纳一个权能。在 32 位架构上这是 16 字节，在 64 位架构上是 32 字节。与任何其他对象一样，CNode 必须通过对适当数量的无类型内存调用 seL4_Untyped_Retype() 来创建（见第 2.4.2 节）。因此，调用者必须拥有对至少 CSpace 大小的无类型内存的权能，并且在现有 CNode 中有足够的空闲权能槽位，seL4_Untyped_Retype() 调用才能成功。

3.1.2 CNode 方法

权能主要通过调用 CNode 方法来管理。

CNode 支持以下方法：

• seL4_CNode_Mint() 从现有权能在指定的 CNode 槽位中创建新权能。新创建的权能的权限可以少于原始权能，且可以有不同的守卫（见第 3.3.1 节）。seL4_CNode_Mint() 还可以从无标记权能创建带标记权能（见第 4.2.1 节）。

• seL4_CNode_Copy() 类似于 seL4_CNode_Mint()，但新创建的权能与原始权能具有相同的标记和守卫。

• seL4_CNode_Move() 在两个指定的权能槽位之间移动权能。不能将权能移动到它当前所在的槽位。

• seL4_CNode_Mutate() 可以类似 seL4_CNode_Move() 移动权能，也可以类似 seL4_CNode_Mint() 减少其权限，但不进行复制。也就是说，如果权能是可撤销的，它仍然可撤销。类似 seL4_CNode_Mint()，它可以用于调整 CNode 权能的守卫。它不能用于标记端点权能。

• seL4_CNode_Rotate() 在三个指定的权能槽位之间移动两个权能。它本质上是两次 seL4_CNode_Move() 调用：一次从第二个指定槽位到第一个，一次从第三个到第二个。第一个和第三个指定槽位可以是相同的，此时其中的权能与第二个槽位中的权能交换。该方法是原子的；要么两个权能都被移动，要么都不移动。

• seL4_CNode_Delete() 从指定槽位移除权能。

• seL4_CNode_Revoke() 等同于对指定权能的每个派生子对象调用 seL4_CNode_Delete()。它对权能本身没有影响，除非在第 3.2 节概述的非常特定的情况下。

• seL4_CNode_SaveCaller() 将当前线程的内核生成的回复权能从其创建的特殊 TCB 槽位移到指定的 CSpace 槽位（仅非 MCS）。

• seL4_CNode_CancelBadgedSends() 取消所有使用与指定权能相同标记和对象的未完成发送。

3.1.3 新重类型化对象的权能

使用 seL4_Untyped_Retype() 将无类型内存重类型化为对象时，对新重类型化对象的权能被放置在由 root、node_index 和 node_depth 参数指定的 CNode 中的连续槽位中。node_offset 参数指定第一个权能将被放置的 CNode 索引。num_objects 参数指定要创建的权能（以及因此对象）的数量。所有槽位必须为空，否则将导致错误。所有生成的权能将被放置在同一个 CNode 中。

3.1.4 权能权限

如前所述，某些权能类型具有关联的访问权限。目前，访问权限与端点（见第 4 章）、通知（见第 5 章）、页（见第 7 章）和回复（见第 4 章）的权能相关联。与权能关联的访问权限决定了可以调用哪些方法。seL4 支持四种访问权限：Read（读）、Write（写）、Grant（授予）和 GrantReply（授予回复）。Read、Write 和 Grant 彼此正交。GrantReply 是 Grant 的较弱形式——例如，如果已经拥有 Grant，是否拥有 GrantReply 无关紧要。每种权限的含义相对于各种对象类型来解释，详见表 3.1。

表 3.1：seL4 访问权限：特定权限授予权能的操作

当对象首次创建时，引用它的初始权能携带最大访问权限集。其他权限较少的权能可以通过 seL4_CNode_Mint() 和 seL4_CNode_Mutate() 等方法从该原始权能制造。如果在这些调用中为目标权能指定了比源权能更大的权限集，目标权限将被静默降级为源权能的权限。

3.1.5 权能派生树

如第 2.4.1 节所述，seL4 在权能派生树中跟踪权能派生。

各种方法，如 seL4_CNode_Copy() 或 seL4_CNode_Mint()，可用于创建派生权能。并非所有权能都支持派生。通常，只有原始权能支持派生调用，但也有例外。表 3.2 汇总了各种权能类型成功进行权能派生必须满足的条件，以及每种情况下权能派生失败如何报告。未列出的权能类型可以派生一次。

图 3.1 展示了一个示例权能派生树，说明了一个标准场景：顶层是一个大型无类型权能，第二层将此权能分割为由各自无类型权能覆盖的两个区域，两者都是第一层的子对象。左边的第三层是第二层无类型权能的副本。无类型权能在复制时始终创建子对象，而非兄弟对象。在此场景中，无类型权能被重类型化为两个独立对象，在第四层创建两个权能，两者分别是对各自对象的原始权能，都是创建它们的那个无类型权能的子对象。

普通原始权能可以有一层派生权能。这些派生权能的进一步副本将创建兄弟对象，在这种情况下仍然在第五层。Endpoint 和 Notification 权能对此方案有一个例外——它们通过标记支持额外的深度层。原始 Endpoint 或 Notification 权能将是无标记的。使用 mint 方法，可以创建具有特定标记的权能副本（见第 4.2.1 节、第 5.1 节）。这个新的、带标记的指向同一对象的权能被视为原始权能（“原始带标记端点权能”），并像其他权能一样支持一层派生子对象。

表 3.2：权能派生

flowchart BT
    root["Untyped"]

    ut2L["Untyped"]
    ut2R["Untyped"]

    ut3L["Untyped"]

    ut2L --> root
    ut2R --> root
    ut3L --> ut2L

    subgraph obj1 ["Object 1"]
        o1orig["original"]
    end

    subgraph obj2 ["Object 2"]
        o2orig["original"]
        o2d1["derived"]
        o2d2["derived"]
        o2d3["derived"]
    end

    subgraph endpoint ["Endpoint"]
        ep_orig_unbadged["original unbadged"]
        ep_derived_unbadged["derived unbadged"]
        ep_orig_badged["original badged"]
        ep_db1["derived badged"]
        ep_db2["derived badged"]
    end

    o1orig --> ut3L
    o2orig --> ut3L
    o2d1 --> o2orig
    o2d2 --> o2orig
    o2d3 --> o2orig

    ep_orig_unbadged --> ut2R
    ep_derived_unbadged --> ep_orig_unbadged
    ep_orig_badged --> ep_orig_unbadged
    ep_db1 --> ep_orig_badged
    ep_db2 --> ep_orig_badged

    o1orig ~~~ o2orig

    style obj1 stroke-dasharray: 5 5
    style obj2 stroke-dasharray: 5 5
    style endpoint stroke-dasharray: 5 5

图 3.1：示例权能派生树——展示从顶层无类型权能派生到 Endpoint 对象的层级结构

3.2 删除与撤销

seL4 中的权能可以被删除和撤销。两种方法主要影响权能，但当删除或撤销导致某个对象的最后一个权能被销毁时，它们可能对系统中的对象产生副作用。

如上所述，seL4_CNode_Delete() 将从指定 CNode 槽位移除权能。通常，仅此而已。然而，如果它是对对象的最后一个有类型权能，该对象现在将被内核销毁，清理所有剩余的内核内引用并准备内存以供重用。

如果要销毁的对象是权能容器，即 TCB 或 CNode，销毁过程将在销毁容器之前删除容器中持有的每个权能。如果所包含的权能是某个对象的最后一个权能，这可能导致进一步的对象销毁。递归是有限的：如果发现指向 CNode 的最后一个权能在容器内，则该 CNode 不会被销毁，而是通过将权能移动到找到的 CNode 中、交换第一个权能并尝试删除交换后的权能来打破递归。实际结果是，删除 CSpace 根 CNode 的最后一个权能不会递归删除整个 CSpace，而是删除根 CNode，树的分支变得不可达。

seL4_CNode_Revoke() 方法将对指定权能的所有 CDT 子对象执行 seL4_CNode_Delete()，但保持权能本身完好无损。如果任何被撤销的子权能是对对象的最后一个权能，将触发相应的销毁操作。

注意：seL4_CNode_Revoke() 在两种特定情况下可能仅部分完成。第一种情况是，作为撤销结果，包含执行撤销的线程 TCB 的最后一个权能（或 TCB 本身的最后一个权能）的 CNode 被删除。在这种情况下，执行撤销的线程在撤销过程中被销毁，撤销未完成。第二种情况是，作为撤销结果，包含撤销目标权能的存储被删除。在这种情况下，执行撤销的权限在操作过程中被移除，操作中途停止。这两种场景都可以通过用户级构造来避免。

注意，对于页表和页目录，seL4_CNode_Revoke() 不会撤销映射到地址空间中的帧权能。它们只会从空间中取消映射。

3.3 CSpace 寻址

执行系统调用时，线程通过在其 CSpace 中给出地址向内核指定要调用的权能。该地址指向调用者 CSpace 中包含要调用权能的特定槽位。

CSpace 设计为允许稀疏性，查找权能地址的过程必须高效。因此，CSpace 实现为带守卫的页表。

如前所述，CSpace 是 CNode 对象的有向图，每个 CNode 是一个槽位表，每个槽位可以为空，或包含权能（可能引用另一个 CNode）。回顾第 2.3 节，CNode 中的槽数必须是 2 的幂。CNode 被称为具有基数（radix），即其大小中 2 的幂次。也就是说，如果 CNode 有 2^k 个槽位，其基数为 k。内核在每个线程的 TCB 中存储对该线程 CSpace 根 CNode 的权能。概念上，CNode 权能不仅存储对其引用的 CNode 的引用，还携带守卫值，在第 3.3.1 节中解释。

3.3.1 权能地址查找

与虚拟内存地址类似，权能地址是一个整数。权能地址不指向物理内存的位置（如虚拟内存地址那样），而是指向权能槽位。当查找用户空间线程提供的权能地址时，内核首先查阅线程 TCB 中定义线程 CSpace 根的 CNode 权能。然后将该 CNode 的守卫值与权能地址的最高有效位进行比较。如果两个值不同，查找失败。否则，内核使用权能地址接下来的基数位作为对 CNode 权能引用的 CNode 的索引。由这些基数位标识的槽位 s 可能包含另一个 CNode 权能或其他内容（包括空）。如果 s 包含 CNode 权能 c 并且权能地址中仍有剩余位（在基数位之后）需要翻译，查找过程从 CNode 权能 c 开始并使用这些剩余位重复。否则，查找过程成功终止；有问题的权能地址指向权能槽位 s。

图 3.2 展示了一个有效的 CSpace，具有以下特征：

• 具有 12 位守卫（设为 0x000）和 256 个槽位的顶层 CNode 对象；
• 具有直接对象引用的顶层 CNode；
• 具有两个第二级 CNode 引用的顶层 CNode；
• 具有不同守卫和槽数的第二级 CNode；
• 包含对顶层 CNode 引用的第二级 CNode；
• 包含对另一个 CNode 引用的第二级 CNode，其中有一些位剩余待翻译；
• 包含对另一个 CNode 引用的第二级 CNode，其中没有剩余位待翻译；
• 第二级 CNode 中的对象引用。

应注意，图 3.2 仅展示什么是可能的，而非通常实用的。虽然示例 CSpace 是合法的，但由于槽数量少和其中存在循环引用，使用起来相当困难。

图 3.2：展示各级对象引用、各种守卫和基数大小以及内部 CNode 引用的 CSpace 示例

3.3.2 权能寻址

权能地址存储在 CPointer（缩写为 CPtr）中，这是一个无符号整数变量。权能按照上述翻译算法进行寻址。两种特殊情况涉及寻址 CNode 权能本身和寻址权能槽位范围。

回顾上述翻译算法将在有地址位剩余待翻译时遍历 CNode 权能。因此，为了寻址可能为 CNode 权能的权能，用户不仅必须提供权能地址，还必须指定权能地址中要翻译的最大位数，称为深度限制。当 CPtr 与深度限制 depth 配对时，仅使用其 depth 个最低有效位进行翻译。

某些方法，如 seL4_Untyped_Retype()，要求用户提供权能槽位范围。这是通过提供基本权能地址（指向范围中的第一个槽位）和窗口大小参数（指定范围中的槽数，地址按基本槽位之后连续排列）来完成的。

图 3.3 描绘了一个示例 CSpace。为了说明这些概念，我们确定此 CSpace 中 10 个权能各自的地址。

• 权能 A：第一个 CNode 具有 4 位守卫（设为 0x0）和 8 位基数。权能 A 位于槽位 0x60，因此，只要它不是 CNode 权能，就可以被任何形如 0x060nnnnn 的地址引用（其中 nnnnn 是任意 5 位十六进制数字序列，因为翻译过程在翻译地址的前 12 位后终止）。为简单起见，我们通常将未使用的地址位设为 0，在此情况下得到的地址为 0x06000000。

• 权能 B：同样，第一个 CNode 具有 4 位守卫（设为 0x0）和 8 位基数。第二个 CNode 通过 L2 CNode Cap 到达。它也有 4 位守卫 0x0，权能 B 位于索引 0x60。因此，权能 B 的地址为 0x00F06000。此地址的翻译在前 24 位后终止。

• 权能 C：此权能通过两个 CNode 寻址。第三个 CNode 通过位于第二个 CNode 索引 0x00 的 L3 CNode Cap 到达。第三个 CNode 没有守卫，权能 C 位于索引 0x60。因此，其地址为 0x00F00060。此地址的翻译后剩余 0 位未翻译。

• 权能 C–G：此权能槽位范围通过提供基本地址（指向包含权能 C 的槽位）0x00F00060 和窗口大小 5 来寻址。

• L2 CNode Cap：回顾要寻址 CNode 权能，用户不仅必须提供权能地址，还必须指定深度限制，即要翻译的最大位数。L2 CNode Cap 位于第一个 CNode 的偏移 0x0F 处，该 CNode 具有 4 位守卫 0x0。因此，它可以被任何形如 0xnnnnn00F 的地址以 12 位深度限制引用，其中 nnnnn 是任意 5 位十六进制数字序列。

• L3 CNode Cap：此权能位于第二个 CNode 的索引 0x00 处，该 CNode 通过 L2 CNode Cap 到达。第二个 CNode 具有 4 位守卫 0x0。因此，该权能可以被任何形如 0xnn00F000 的地址以 24 位深度限制引用，其中 nn 是任意 2 位十六进制数字序列。

综上所述，要引用 CSpace 中的任何权能（或槽位），用户必须提供其地址。当权能可能是 CNode 时，用户还必须提供深度限制。要指定权能槽位范围，用户提供起始地址和窗口大小。

[图 3.3：一个任意的 CSpace 布局]

3.4 查找失败描述

当权能查找失败时，失败描述将在 IPC 缓冲区中提供给调用线程或线程的异常处理程序。描述格式始终相同，但根据错误发生的方式，可能出现在 IPC 缓冲区的不同偏移处。

描述格式如下所述。第一个字指示查找失败的类型，后续字的含义取决于此。

3.4.1 无效根

CSpace CPtr 根（要在其中查找权能的）无效。例如，该权能不是 CNode 权能。

3.4.2 缺失权能

调用所需的权能不存在或没有足够的权限。

3.4.3 深度不匹配

解析权能时，遍历的 CNode 解析的位数超过了 CPtr 中剩余待解码的位数，或者仍有剩余位待查找时遇到了非 CNode 权能。

3.4.4 守卫不匹配

解析权能时，遍历的 CNode 的守卫大小大于剩余位数，或者 CNode 的守卫与 CPtr 中正在解析的下一位不匹配。

第4章 消息传递（IPC）

seL4 微内核提供了一种消息传递 IPC（Inter-Process Communication，进程间通信）机制，用于线程之间的通信。同样的机制也用于与内核提供的服务进行通信。

消息通过调用内核对象的能力（capability）来发送。发送到端点（Endpoint）的消息是发往其他线程的，而发送到其他对象的消息则由内核处理。本章介绍通用的消息格式、端点，以及如何使用它们进行应用程序之间的通信。

4.1 消息寄存器

每条消息包含若干个消息字（message word）和可选的若干个能力。消息字通过放入线程的消息寄存器（message register）中来发送或接收。消息寄存器按编号排列，前几个消息寄存器使用物理 CPU 寄存器实现，其余则由一块称为 IPC 缓冲区（IPC buffer）的固定内存区域支持。这种设计是为了效率：非常短的消息无需使用内存。IPC 缓冲区分配给调用线程（参见第 6.1 节和第 10.3.7.10 节）。

每条 IPC 消息还有一个标签（seL4_MessageInfo_t 结构体）。标签由四个字段组成：标签（label）、消息长度（messageLength）、能力数量（extraCaps 字段）和 capsUnwrapped 字段。消息长度和能力数量决定了发送线程希望传输的消息寄存器和能力的数量，或者实际传输的消息寄存器和能力的数量。内核不解释标签字段，它作为消息的第一个数据载荷原样传递。例如，标签可用于指定请求的操作。capsUnwrapped 字段仅用于接收端，用于指示能力被接收的方式。该字段在第 4.2.2 节中描述。

内核假定 IPC 缓冲区包含一个如表 4.1 所定义的 seL4_IPCBuffer 类型的结构体。内核尽可能多地使用物理寄存器来传输 IPC 消息。当传输的参数数量超过可用的物理消息寄存器时，内核开始使用 IPC 缓冲区的 msg 字段来传输参数。但是，它会在该数组中为物理消息寄存器留出空间。例如，如果一个 IPC 传输或内核对象调用需要 4 个消息寄存器（而该架构上只有 2 个物理消息寄存器可用），则参数 1 和 2 将通过消息寄存器传输，参数 3 和 4 将放在 msg[2] 和 msg[3] 中。这允许用户级对象调用桩（stub）根据需要将物理寄存器中传递的参数复制到 msg 数组中留出的空间。标签字段的情况类似。seL4_IPCBuffer 结构体中为此字段留出了空间，内核会忽略它。用户级桩可能希望将消息标签从 CPU 寄存器复制到此字段，尽管内核提供的用户级桩并未这样做。

表 4.1：seL4_IPCBuffer 结构体的字段。注意 badges 和 caps 使用结构体中的同一块内存区域。

4.2 端点

端点（Endpoint）允许在两个线程之间传输少量数据和能力（即 IPC 缓冲区）。端点对象直接使用第 2.2 节中描述的 seL4 系统调用来调用。

IPC 端点使用会合（rendezvous）模型，因此是同步且阻塞的。端点对象可以将线程排队等待发送或接收。如果没有接收者就绪，执行 seL4_Send() 或 seL4_Call() 系统调用的线程将在队列中等待第一个可用的接收者。同样，如果没有发送者就绪，执行 seL4_Recv() 系统调用或 seL4_ReplyRecv() 后半部分的线程将等待第一个可用的发送者。

在没有写（Write）权限的情况下尝试发送（Send）或调用（Call）将失败并返回错误。对于发送（Send），该错误会被忽略（内核不允许回复）。因此，无法得知发送是否因缺少权限而失败。另一方面，使用没有读（Read）权限的端点能力调用 seL4_Recv() 将引发故障（fault），参见第 6.2 节。这是因为否则错误消息将与通过端点从其他线程接收的正常消息无法区分。

4.2.1 端点标记

端点能力可以通过铸造（mint）操作创建带有标记（badge）的新端点能力，标记是调用铸造操作者选择的数据字。当使用带标记的能力向端点发送消息时，标记会传输到接收线程的标记寄存器（badge register）中。

标记为零的端点能力称为无标记（unbadged）能力。此类能力可以通过对包含该能力的 CNode 调用 seL4_CNode_Mint() 来添加标记。带有标记的端点能力不能被取消标记、重新标记或用于创建具有不同标记的子能力。

在 32 位平台上，只有标记的低 28 位可用。内核将静默忽略高 4 位的任何使用。在 64 位平台上，标记有 64 位可用。

4.2.2 能力转移

消息可以包含能力，这些能力将被复制到接收者，前提是发送线程调用的端点能力具有授予（Grant）权限。尝试使用没有 Grant 权限的端点能力发送能力将导致传输原始消息，而不进行任何能力转移。

要发送的能力在发送线程的 IPC 缓冲区的 caps 字段中指定。该数组中的每个条目被解释为发送线程能力空间中的 CPtr。要发送的能力数量在消息标签的 extraCaps 字段中指定。

接收者通过 IPC 缓冲区中的三个字段指定它愿意接收能力的槽（slot）：receiveCNode、receiveIndex 和 receiveDepth。这些字段分别指定根 CNode、能力地址和要解析的位数，以找到放置能力的槽。能力寻址在第 3.3.2 节中描述。

请注意，接收线程只能指定一个接收槽，而发送线程可以在消息中包含多个能力。包含多个能力的消息可以被内核对象解释。在某些情况下，如果消息中的一些额外能力可以被解包（unwrapped），它们也可以发送给接收线程。

如果消息中的第 n 个能力引用了消息发送所经过的端点，则该能力被解包：其标记被放入接收者的 badges 数组的第 n 个位置，内核在消息标签的 capsUnwrapped 字段中设置第 n 位（从最低有效位计数）。该能力本身不被传输，因此接收槽可用于另一个能力。

未被解包的能力通过将其从发送者的 CNode 槽复制到接收者的 CNode 槽来传输。发送者保留对已发送能力的访问权限。

如果接收者收到一条消息，其标签的 extraCaps 为 2，capsUnwrapped 为 2，则消息中的第一个能力被转移到指定的接收槽，第二个能力被解包，其标记被放入 badges[1]。发送者消息中可能还有第三个无法解包的能力。

4.2.3 错误

能力传输中的错误可能发生在两个阶段：发送阶段或接收阶段。

在发送阶段，在发送在内核中启动之前，调用者尝试发送的所有能力都会被查找以确认它们存在。如果查找因任何原因失败，seL4_Send() 和 seL4_Call() 系统调用立即中止，不进行任何 IPC 或能力转移。系统调用将返回第 10.1 节中描述的查找失败错误。

在接收阶段，seL4 按发送线程 IPC 缓冲区 caps 数组中的顺序传输能力，并在遇到错误时立即终止。可能的错误条件包括：

• 源能力无法被查找。虽然在发送线程执行发送系统调用时检查了源能力的存在，但此错误仍可能发生。发送线程可能在端点上阻塞了一段时间才与接收线程配对。在此期间，其 CSpace 可能已发生变化，源能力指针可能不再有效。
• 目标槽无法被查找。与发送系统调用不同，seL4_Recv() 系统调用在启动接收操作之前不会检查目标槽是否存在且为空。因此，如果目标槽无效，seL4_Recv() 系统调用不会因错误而失败，而是会继续传输带标记的能力，直到尝试将能力保存到目标槽为止。
• 正在传输的能力无法派生。详情参见第 3.1.5 节。

错误不会使整个传输无效，只会提前终止它。在失败之前处理的能力仍然被传输，接收者 IPC 缓冲区中的 extraCaps 字段被设置为失败前传输的能力数量。在上述任何情况下，都不会向接收线程返回错误消息。

4.2.4 调用与回复

如第 2.2 节所述，当用户在端点能力上调用 seL4_Call() 时，会执行一些特定的操作。首先，调用（Call）将执行与普通 seL4_Send() 完全相同的操作。然后，在会合和所有正常的 IPC 过程发生之后，seL4_Call() 不会直接返回给调用者，而是检查调用的端点能力上是否存在 Grant 或 GrantReply 权限：

• 如果不存在，调用者线程被挂起，就像对它调用了 seL4_TCB_Suspend() 一样。调用的发送部分仍将照常执行。
• 如果存在，则在接收者 TCB 的特定槽中设置一个回复能力（reply capability）。该回复能力的 Grant 权限通过复制接收者在 seL4_Recv() 中调用的端点能力的 Grant 权限来设置。然后，调用者线程被阻塞，等待回复。

回复能力直接指向调用者线程，一旦调用完成，就与原始端点完全无关。即使后者被销毁，回复能力仍然存在并指向仍在等待回复的调用者。

生成的回复能力可以通过 seL4_Reply() 就地调用（在特定的 TCB 槽中），或者使用 seL4_CNode_SaveCaller() 保存到可寻址的槽中以供稍后通过 seL4_Send() 调用。特定槽不能直接用任何 CPtr 寻址，因为它不属于任何 CSpace。

回复能力的调用方式与在端点上发送普通消息相同。回复能力隐式具有写（Write）权限，因此消息总能通过。在回复中转移能力只有在回复能力具有 Grant 权限时才能进行，其方式与第 4.2.2 节中描述的普通 IPC 传输完全相同。

与普通端点传输的主要区别在于，内核保证调用回复能力不会阻塞：如果你拥有一个回复能力，那么它指向的线程正在等待回复。然而，回复能力是一种非拥有引用（non-owning reference），这与所有其他能力不同。这意味着如果调用者线程被销毁或以任何可能导致回复不可能的方式被修改（例如通过 seL4_TCB_Suspend() 挂起），内核将立即销毁回复能力。

一旦回复能力被调用，调用者将收到消息，就像它一直在执行 seL4_Recv() 并刚刚收到消息一样。特别是，它将重新开始运行。

seL4_Call() 操作不仅出于效率原因（将两个操作合并为单个系统调用）。它与直接跟随 seL4_Send() 的 seL4_Recv() 不同，这允许某些系统设置以比传统设置少得多的配置工作得更高效。特别是，保证调用者收到的回复来自接收调用的线程，而无需检查任何类型的标记。

第5章 通知

通知（Notification）是一种简单的、非阻塞的信号机制，在逻辑上表示一组二进制信号量。

5.1 通知对象

通知对象包含一个数据字，称为通知字（notification word）。此类对象支持两种操作：seL4_Signal() 和 seL4_Wait()。

通知能力可以使用 seL4_CNode_Mint() 添加标记，类似于端点能力（参见第 4.2.1 节）。与端点能力一样，带标记的通知能力不能被取消标记、重新标记或用于创建具有不同标记的子能力。

5.2 信号、轮询与等待

seL4_Signal() 方法通过将调用的通知能力的标记与通知字进行按位或（OR）操作来更新通知字。它还会解除阻塞等待该通知的第一个线程（如果有的话）。因此，seL4_Signal() 的工作方式类似于同时给多个信号量发信号（由标记中设置的位指示的信号量）。如果信号发送者能力是无标记或零标记的，该操作仅退化为唤醒等待该通知的第一个线程（另见下文）。

seL4_Wait() 方法的工作方式类似于对信号量集的 select 风格等待：如果调用 seL4_Wait() 时通知字为零，调用者将阻塞。否则，调用立即返回，将通知字设置为零，并向调用者返回之前通知字的值。

seL4_Poll() 与 seL4_Wait() 相同，区别在于如果没有待处理的信号（通知字为 0），调用将立即返回而不阻塞。

如果在调用 seL4_Signal() 时有线程正在等待通知对象，则队列中的第一个线程收到通知。所有其他线程继续等待，直到下次通知被发出信号。

5.3 绑定通知

通知对象和 TCB 可以通过 seL4_TCB_BindNotification() 调用以一对一关系绑定在一起。当通知绑定到 TCB 时，即使线程正在从 IPC 端点接收消息，对该通知对象的信号也会被送达。为了区分接收到的消息是通知还是 IPC，开发者应检查标记值。通过为绑定通知的能力预留特定的标记（或标记范围）——与端点标记不同——可以确定消息来源。

一旦通知被绑定，唯一可以对通知执行 seL4_Wait() 的线程就是绑定的线程。

第6章 线程与执行

6.1 线程

seL4 提供线程（thread）来表示执行上下文。在内核的 MCS 配置下，调度上下文（scheduling context）用于管理处理器时间。在没有 MCS 的情况下，处理器时间也由线程抽象表示。线程在 seL4 中由其线程控制块对象（TCB，Thread Control Block）表示。

在 MCS 下，调度上下文由调度上下文对象（SCO，Scheduling Context Object）表示，线程除非绑定到调度上下文或接收调度上下文，否则不能运行。

6.1.1 线程控制块

每个 TCB 都有一个关联的 CSpace（参见第 3 章）和 VSpace（参见第 7 章），它们可以与其他线程共享。TCB 还可以有一个 IPC 缓冲区（参见第 4 章），用于在 IPC 或内核对象调用期间传递超出架构定义的消息寄存器容量的额外参数。虽然线程不一定必须有 IPC 缓冲区，但没有它将无法执行大多数内核调用，因为它们需要能力传输。每个线程属于且仅属于一个安全域（security domain）（参见第 6.3 节）。

6.1.2 线程创建

与其他对象一样，TCB 使用 seL4_Untyped_Retype() 方法创建（参见第 2.4 节）。新创建的线程初始时不活跃。通过使用 seL4_TCB_SetSpace() 或 seL4_TCB_Configure() 方法设置其 CSpace 和 VSpace，然后调用 seL4_TCB_WriteRegisters() 并传入初始栈指针和指令指针来配置线程。线程可以通过将 seL4_TCB_WriteRegisters() 调用中的 resume_target 参数设置为 true 来激活，或者通过单独调用 seL4_TCB_Resume() 方法来激活。这两种方法都将线程置于可运行状态。

在非 MCS 配置的内核中，这将导致线程立即被添加到调度器中。在 MCS 内核上，线程只有拥有调度上下文对象才会开始运行。

在 SMP 配置的内核中，线程将在与其亲和性（affinity）对应的节点上恢复运行。对于非 MCS 配置，默认的线程亲和性是线程 TCB 对象创建所在的节点，可以使用 seL4_TCB_SetAffinity() 显式设置亲和性。在 MCS 配置下，亲和性从调度上下文对象派生（参见第 6.1.9 节）。

6.1.3 线程停用

seL4_TCB_Suspend() 方法停用线程。挂起的线程稍后可以恢复。可以使用 seL4_TCB_ReadRegisters() 和 seL4_TCB_CopyRegisters() 方法获取其挂起状态。它们还可以被重新配置和重用，或者在不需要时无限期保持挂起状态。当指向线程 TCB 的最后一个能力被删除时，线程将自动挂起。

6.1.4 亲和性

亲和性值如何映射到特定平台上的特定节点（核心、hart）是架构和平台相关的。不保证亲和性值在不同平台之间兼容。

6.1.5 调度

seL4 使用抢占式、无滴答（tickless）调度器，具有 256 个优先级（0 — 255）。所有线程都有一个最大受控优先级（MCP，Maximum Controlled Priority）和一个优先级，后者是线程的有效优先级。当线程修改另一个线程的优先级（包括自身）时，它必须提供一个线程能力，从中获取 MCP。线程只能将优先级和 MCP 设置为小于或等于所提供线程 MCP 的值。初始任务以系统最高优先级（seL4_MaxPrio）的 MCP 和优先级启动。线程优先级和 MCP 可以使用 seL4_TCB_SetSchedParams()、seL4_TCB_SetPriority() 和 seL4_TCB_SetMCPriority() 方法设置。

在符合调度条件的线程中，选择处于可运行状态的最高优先级线程。线程优先级（seL4_PrioProps_t 结构体）由以下两个值组成：

• 优先级（Priority）：线程被调度时将使用的优先级。
• 最大受控优先级（MCP）：线程可以将自身或其他线程设置到的最高优先级。

6.1.6 MCS 调度

本节仅适用于启用了 MCS 的配置，其中线程必须有一个可用的调度上下文对象才能被调度器接纳。

6.1.7 调度上下文

对 CPU 执行时间的访问通过调度上下文对象控制。调度上下文配置了一个预算（budget，b）和周期（period，p）的元组，两者均以微秒为单位，通过 seL4_SchedControl_Configure_Flags() 设置（参见第 6.1.9 节）。元组 (b, p) 构成线程执行的上限——内核不允许线程在每 p 微秒中运行超过 b 微秒。然而，b/p 并不代表执行的下限，因为线程必须具有所有可运行线程中最高或相等的优先级才能保证被调度，而且内核不进行准入测试。因此，所有参数的集合不一定可调度。如果多个线程同时有可用的预算，它们按先入先出（FIFO）调度，一旦预算耗尽，则应用轮转（round-robin）调度。

有资格被调度器选中的调度上下文，即具有可用预算的调度上下文，称为活跃（active）调度上下文。预算计费和补充规则对于轮转线程和偶发（sporadic）线程是不同的。对于轮转线程，每次当前节点的调度上下文发生变化时都会计费预算，直到耗尽然后立即重新填充。

b == p 的线程被视为轮转线程，其中 b 作为时间片（timeslice）。否则，内核使用偶发服务器（sporadic server）来强制执行时间隔离，这强制了对于所有可能的 p，b/p 不能超出的属性。理论上，偶发服务器通过以下算法提供时间隔离——防止线程超出其分配的预算：

• 当线程在当前时间 T 开始执行时，记录 Ts。
• 当线程停止执行（阻塞或被抢占）时，在 Ts + p 处调度一个补充，补充量为消耗的时间 (T − Ts)，并从当前正在使用的补充中减去该量。

seL4 通过在每个调度上下文中维护一个有序的偶发补充列表——简称为 refill——来实现此算法。每个补充包含一个元组，包括其可使用的时间（rTime）和该补充的数量（rAmount）。当线程执行时，它持续从补充列表头部的 rAmount 中消耗预算。如果 rTime 在未来，绑定到该调度上下文的线程被放入等待更多预算的线程队列中。

轮转线程的处理方式与偶发线程相同，除了一方面：预算的计费方式。轮转线程只有两个 refill，两者始终可用。当轮转线程停止执行时，预算从头部补充移动到尾部补充。一旦头部预算耗尽，线程将从其优先级的调度队列中移除并追加到尾部。

偶发线程的行为取决于可用的补充数量，该数量必须有界。开发者有两个选项来配置补充列表的大小：

• 单个调度上下文中的最大 refill 数量由创建调度上下文时（通过 seL4_Untyped_Retype()）的大小决定。
• 每个调度上下文参数 extra_refills，限制该特定调度上下文的 refill 数量。此值被添加到基数 2 上，并受调度上下文大小的限制。

执行时间短（例如中断处理程序）且不经常被抢占的线程应具有较少的 refill，而运行时间较长、b 值较大的线程应具有较高的值。绑定到具有 0 个额外 refill 的调度上下文的线程将周期性运行——使用其头部补充或调用 yield 的任务在下一个周期开始之前不会被再次调度。

鉴于补充数量有限，如果节点的 SC 发生变化且离开的 SC 没有足够的空间存储新的补充，则通过移除当前补充来创建空间，这可能导致抢占（如果下一个补充尚不可用）。配置了更多 refill 的调度上下文将消耗更接近其全部预算，因为它们可以更频繁地被抢占和切换线程而不会填满其补充队列。然而，调度开销会更高，因为补充列表可能会出现碎片化。

每当线程执行时，它都从其当前调度上下文中消耗预算。系统调用 seL4_Yield() 可用于放弃任何剩余预算并阻塞，直到下一个补充准备好使用。

线程可以使用 seL4_TCB_Configure() 或 seL4_SchedContext_Bind() 绑定到调度上下文，两种调用具有相同的效果，尽管 seL4_TCB_Configure() 允许在仅一次内核入口中设置更多线程字段。当线程绑定到调度上下文时，如果它处于可运行状态且调度上下文是活跃的，它将被添加到调度器中。

6.1.8 被动线程

可以使用 seL4_SchedContext_UnbindObject() 将线程从调度上下文解绑。这与挂起线程不同，在端点或通知队列中阻塞等待的线程将保留在队列中，仍然可以接收消息和信号。但是，解绑的线程在收到调度上下文之前将无法再次被调度。

没有调度上下文的线程称为被动线程（passive thread），因为它们在没有其他线程的操作下无法执行。

6.1.9 调度上下文创建

与其他对象一样，调度上下文使用 seL4_Untyped_Retype() 从未类型化内存创建。创建时，调度上下文为空，表示 0% 的 CPU 执行时间。要使用参数填充调度上下文，必须调用相应的 SchedControl 能力，该能力提供对单个节点上 CPU 时间管理的访问。每个节点的调度控制能力在运行时提供给初始任务。线程在其调度上下文配置的节点上运行。然后可以使用 seL4_SchedControl_ConfigureFlags() 设置和更新调度上下文参数，该方法允许指定预算和周期以及以下标志的按位或组合：

• seL4_SchedContext_Sporadic：仅根据偶发服务器算法约束执行时间，而不是连续的恒定带宽。

内核不进行任何可调度性测试，因为任务准入留给用户级策略，可以在线或离线、静态或动态地进行，或者根本不进行。

6.1.10 调度上下文捐赠

除了通过 seL4_SchedContext_Bind() 和 seL4_SchedContext_UnbindObject() 显式绑定和移除调度上下文之外，调度上下文还可以通过 IPC 在线程之间移动。当系统调用 seL4_Call() 和 seL4_NBSendRecv() 用于与被动线程通信时，调度上下文会隐式捐赠。当活跃线程使用 seL4_Call() 调用端点并与被动线程会合时，活跃线程的调度上下文被捐赠给被动线程。生成的回复能力确保被调用者仅仅是借用调度上下文：当回复能力被发送回复消息消耗时，调度上下文将返回给调用者。如果回复能力被撤销，且被调用者持有调度上下文，调度上下文将返回给调用者。然而，如果在深度调用链中，调用链中间的回复能力被撤销，使得被调用者不拥有调度上下文，则该线程将从调用链中移除，调度上下文将保留在原处。如果接收者没有提供回复对象来跟踪捐赠（即使用 seL4_Wait() 而不是 seL4_Recv()），调度上下文捐赠将不会发生，但消息会被送达。被动接收者将被设置为不活跃，因为它没有调度上下文。

考虑一个例子：线程 A 调用线程 B，线程 B 调用线程 C。如果在 C 持有调度上下文时，B 对 A 的回复能力被撤销，则调度上下文将保留在 C 处。然而，A 和 C 之间将保留调用链，因此如果 C 的回复能力被撤销或被调用，调度上下文将返回给 A。

seL4_NBSendRecv() 也可能导致调度上下文捐赠。如果操作的非阻塞发送阶段导致消息送达被动线程，调度上下文将捐赠给该被动线程，执行系统调用的线程在接收阶段在接收端点上变为被动。不生成回复能力，因此不能保证调度上下文会返回，这增加了记账复杂性，但允许数据流式架构而非远程过程调用。注意 seL4_Call() 也不保证调度上下文的返回：这本质上是一个可信操作，因为服务器可能永远不回复并返回调度上下文。

调度上下文也可以使用 seL4_SchedContext_Bind() 绑定到通知对象，并使用 seL4_SchedContext_UnbindObject() 解绑。如果信号被送达一个通知对象，且有一个被动线程阻塞等待它，被动线程将收到绑定到该通知对象的调度上下文。当线程在通知对象上阻塞时，调度上下文被返回。此功能允许被动服务器使用通知绑定（参见第 5.3 节）。如果调度上下文同时绑定到通知对象和线程，其行为将与被动服务器相同：当线程在绑定的通知对象上阻塞时，调度上下文将从线程解绑。这在启动被动服务器或处理超时异常时很有用。

调度上下文可以使用 seL4_SchedContext_Unbind() 从所有对象解绑（通知对象和通过捐赠绑定或接收调度上下文的 TCB）。

被动线程将在调度上下文配置的 CPU 节点上运行，并在 IPC 时迁移。

6.1.11 调度算法

只有具有活跃调度上下文的线程才有资格被调度。在符合调度条件的线程中，选择处于可运行状态的最高优先级线程。

具有足够最大受控优先级并拥有适当调度上下文能力的线程可以操作调度器，并使用 IPC 实现用户级调度器。

调度上下文提供对 CPU 执行时间上限的访问，但线程何时执行由线程优先级决定。因此，对 CPU 的访问是线程 MCP、调度上下文和 SchedControl 能力的函数。内核将强制线程在任何给定周期内不超过其调度上下文中的预算，并确保最高优先级线程始终运行，但系统设计者需要确保整个系统是可调度的。

6.1.12 异常

每个线程有两个关联的异常处理端点：一个标准异常处理端点和一个超时异常处理端点，后者仅 MCS 可用。如果线程引发异常，内核会创建一条包含相关详细信息的 IPC 消息并将其发送到端点。该线程然后可以采取适当的操作。故障 IPC 消息在第 6.2 节中描述。

标准异常处理端点可以使用 seL4_TCB_SetSpace() 或 seL4_TCB_SetSchedParams() 方法设置，而超时异常处理端点可以使用 seL4_TCB_SetTimeoutEndpoint()（仅 MCS）设置。通过这些方法，可以将异常处理器的能力地址与线程关联。然后使用此地址查找处理端点，并将端点能力安装到线程的内核 CNode 中。对于没有异常处理器的线程，可以使用空能力（null capability），但后果因异常处理器类型而异。在引发异常之前，处理能力会被验证。内核不执行另一次查找，而是检查该能力是否为具有正确权限的端点。

异常端点必须具有写（Write）权限以及 Grant 或 GrantReply 权限。回复异常消息将重新启动线程。对于某些异常类型，回复消息的内容可用于设置正在重启的线程的寄存器值。详情参见第 6.2 节。

6.1.12.1 标准异常

标准异常处理器在线程触发无法在没有其他线程操作的情况下恢复的故障时使用。例如，如果线程由于未映射的虚拟内存页引发故障，线程在页面被映射之前无法继续前进。如果线程在标准异常处理器设置为空能力时遇到会触发标准异常处理器的故障，内核将暂停该线程，线程将不再运行。这是因为没有其他线程的操作，标准异常无法恢复。因此，没有标准异常处理器的线程应被信任为完全不会发生故障。

标准异常处理器可以是被动的，在这种情况下，它们将在故障线程的调度上下文上运行。

6.1.12.2 超时异常（仅 MCS）

当线程尝试运行但没有可用预算，且该线程具有有效的超时异常处理能力时，会引发超时故障。超时故障的处理不是强制性的：如果线程没有超时故障处理器，则不会引发故障，线程将在预算补充后继续运行。这允许对时间敏感的线程处理预算超支，而其他线程可以忽略它们。

超时故障是按线程注册的，这意味着虽然客户端可能没有超时故障处理器，但服务器可以有，允许单线程、时间敏感的被动服务器使用超时异常处理器从恶意或不受信任的客户端（其预算在服务器完成请求期间过期）中恢复。超时故障处理器可以访问服务器回复对象并向客户端回复错误，然后重置服务器以处理下一个客户端请求。如果向嵌套服务器发送回复消息并返回一个没有可用预算的调度上下文，且嵌套服务器也有超时故障处理器，则将生成另一个超时故障。

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

线程的寄存器可以使用 seL4_TCB_ReadRegisters() 和 seL4_TCB_WriteRegisters() 方法读取和写入。对于某些寄存器，内核会静默屏蔽某些位或位范围，并强制它们包含特定值，以确保它们不能被恶意设置为会危及运行系统的值，或者遵守架构规范所规定的特定值。寄存器内容通过 IPC 缓冲区传输。

6.2 故障

线程的操作可能导致故障（fault）。故障被递送到线程的异常处理器，以便它可以采取适当的操作。故障类型在消息标签中指定，为以下之一：

• seL4_Fault_CapFault
• seL4_Fault_VMFault
• seL4_Fault_UnknownSyscall
• seL4_Fault_UserException
• seL4_Fault_TimeoutFault
• seL4_Fault_NullFault（表示没有发生故障，这是一条正常的 IPC 消息）
• seL4_Fault_VGICMaintenence
• seL4_Fault_VPPIEvent
• seL4_Fault_VCPUFault
• seL4_Fault_DebugException

故障的递送方式模仿了故障线程的调用（Call）。这意味着要发送故障消息，故障端点必须具有写（Write）权限以及 Grant 或 GrantReply 权限。如果不是这种情况，将发生双重故障（通常线程会被简单地挂起）。

6.2.1 能力故障

能力故障（capability fault）可能发生在两个地方。首先，当 seL4_Call() 或 seL4_Send() 系统调用引用的能力查找失败时会发生能力故障（对无效能力的 seL4_NBSend() 调用会静默失败）。在这种情况下，发生故障的能力可能是被调用的能力，或者是 IPC 缓冲区 caps 字段中传递的额外能力。其次，当对不存在的能力、不是端点或通知能力、或者没有接收权限的能力调用 seL4_Recv() 或 seL4_NBRecv() 时会发生能力故障。

回复故障 IPC 将重新启动故障线程。IPC 消息的内容如表 6.1 所示。

表 6.1：IPC 消息的内容。

6.2.2 未知系统调用

当线程执行 seL4 未知的系统调用号时发生此故障。故障线程的寄存器集被传递给线程的异常处理器，以便它可以（例如）在线程被虚拟化时模拟该系统调用。

回复故障 IPC 允许重新启动线程和/或修改线程的寄存器集。如果回复的标签为零，则线程将被重启。此外，如果消息长度非零，故障线程的寄存器集将被更新。在这种情况下，更新的寄存器数量由消息标签的 length 字段控制。

6.2.3 用户异常

用户异常（user exception）用于传递架构定义的异常。例如，如果用户线程尝试除以零，则可能发生此类异常。

回复故障 IPC 允许重新启动线程和/或修改线程的寄存器集。如果回复的标签为零，则线程将被重启。此外，如果消息长度非零，故障线程的寄存器集将被更新。在这种情况下，更新的寄存器数量由消息标签的 length 字段控制。

6.2.4 调试异常：断点和观察点

调试异常（debug exception）用于向线程传递与跟踪和调试相关的事件。断点（breakpoint）、观察点（watchpoint）、跟踪事件和指令性能采样事件都是示例。当内核配置为包含这些功能时（设置了 CONFIG_HARDWARE_DEBUG_API），这些事件对用户空间线程可用。硬件调试扩展 API 在内核已移植的以下平台子集上受支持：

• PC99：IA-32 和 x86_64
• Sabrelite（i.MX6）
• Jetson TegraK1
• HiSilicon Hikey
• Raspberry Pi 3
• Odroid-X（Exynos4）
• Xilinx zynq7000

可用硬件调试资源的信息以以下常量的形式呈现：

seL4_NumHWBreakpoints：定义可用硬件断点寄存器的总数，包括硬件平台上可用的所有类型。例如，在 Arm Cortex A7 上，有 6 个独占指令断点寄存器和 4 个独占数据观察点寄存器，总共 10 个监视寄存器。因此在此平台上，seL4_NumHWBreakpoints 定义为 10。指令断点寄存器始终被分配较低的 API-ID，数据观察点始终在其之后分配。

此外，为每个目标平台定义了 seL4_NumExclusiveBreakpoints、seL4_NumExclusiveWatchpoints 和 seL4_NumDualFunctionMonitors，以反映特定类型的可用硬件断点/观察点数量。

seL4_NumExclusiveBreakpoints：定义只能在指令执行时生成故障的硬件寄存器数量。目前仅在 Arm 平台上设置。第一个独占断点的 API-ID 由 seL4_FirstBreakpoint 给出。如果没有指令断点独占寄存器，seL4_NumExclusiveBreakpoints 将设置为 0，seL4_FirstBreakpoint 将设置为 -1。

seL4_NumExclusiveWatchpoints：定义只能在数据访问时生成故障的硬件寄存器数量。目前仅在 Arm 平台上设置。第一个独占观察点的 API-ID 由 seL4_FirstWatchpoint 给出。如果没有数据断点独占寄存器，seL4_NumExclusiveWatchpoints 将设置为 0，seL4_FirstWatchpoint 将设置为 -1。

seL4_NumDualFunctionMonitors：定义能够在任一类型访问上生成故障的硬件寄存器数量——即寄存器同时支持指令和数据断点。目前仅在 x86 平台上设置。第一个双功能监视器的 API-ID 由 seL4_FirstDualFunctionMonitor 给出。如果没有双功能断点寄存器，seL4_NumDualFunctionMonitors 将设置为 0，seL4_FirstDualFunctionMonitor 将设置为 -1。

表 6.2：调试故障消息布局。对于单步故障，寄存器 API-ID 不会从内核的故障消息中返回。

6.2.5 调试异常：单步执行

内核在配置为支持时（设置了 CONFIG_HARDWARE_DEBUG_API），提供对用户空间线程硬件单步执行的支持。为此，它暴露了 seL4_TCB_ConfigureSingleStepping 调用。

调用者应选择与指令断点对应的 API-ID，用于设置单步执行功能（即 API-ID 从 0 到 seL4_NumExclusiveBreakpoints - 1）。然而，并非所有硬件平台都需要实际的硬件断点寄存器来提供单步执行功能。如果调用者的硬件平台需要使用硬件断点寄存器，它将使用 bp_num 中给定的断点寄存器，并在 bp_was_consumed 中返回 true。如果底层平台不需要硬件断点来提供单步执行，seL4 将在 bp_was_consumed 中返回 false 并保持 bp_num 不变。

如果 bp_was_consumed 为 true，调用者在通过后续调用 seL4_TCB_ConfigureSingleStepping 禁用单步执行并释放该寄存器，或通过 n_instr 为 0 的故障回复之前，不应尝试重新配置 bp_num 用于断点或观察点用途。将 num_instructions 设置为 0 可禁用单步执行。

在需要配置实际硬件寄存器来实现单步执行功能的架构上，seL4 将限制可配置为单步执行器的寄存器数量，在任何给定时间最多为一个。当前配置用于单步执行的寄存器（如果有的话）将是单步调试故障回复中隐式的 bp_num 参数。

内核的单步执行还支持在执行一定数量的指令后递送单步故障消息。单步执行时 Num_instructions 应设置为 1，或者设置为任何非零整数值以在执行该数量的指令后恢复单步执行。此执行计数也可以在单步调试故障的故障回复中设置。

表 6.3：单步故障消息布局。

6.2.6 超时故障（仅 MCS）

当线程消耗完所有预算且具有非空能力的超时故障处理器时，会引发超时故障（timeout fault）。它们允许超时异常处理器采取一些操作来恢复线程，并递送一条包含调度上下文数据字的消息，以及自上次该调度上下文上发生超时故障以来消耗的时间量，或自上次调用 seL4_SchedContext_YieldTo() 或 seL4_SchedContext_Consumed() 以来消耗的时间量。超时异常处理器可以使用与第 6.1.13 节所述相同的格式，通过设置寄存器来回复时间故障。

表 6.4：32 位架构上的超时故障结果。

6.2.7 VM 故障

线程导致缺页故障。回复故障 IPC 将重新启动线程。IPC 消息的内容如下所示。

表 6.5：所有架构上的 VM 故障结果。

6.2.8 ARM 虚拟化故障

启用了虚拟机监控器（hypervisor）支持的 Arm 可以生成额外的异常，参见第 6.4.1 节。回复故障 IPC 将重新启动 VCPU 线程。IPC 消息的内容如下所示。

表 6.6：seL4_Fault_VGICMaintenance。

表 6.7：seL4_Fault_VPPIEvent。

表 6.8：seL4_Fault_VCPUFault。

6.3 域

域（domain）用于隔离独立的子系统，以限制它们之间的信息流。内核根据固定的、时间触发的调度在域之间切换。固定调度通过常量 CONFIG_NUM_DOMAINS 和全局变量 ksDomSchedule 编译到内核中。

一个线程属于且仅属于一个域，且仅在该域活跃时运行。seL4_DomainSet_Set() 方法更改线程的域。调用者必须拥有域能力（Domain cap）和线程的 TCB 能力。初始线程以域能力启动（参见第 4.1 节）。

6.4 虚拟化

硬件执行虚拟化在特定的 Arm 和 x86 平台上受支持。接口通过一系列内核对象、调用和系统调用暴露，允许用户利用硬件虚拟化功能。

硬件虚拟化允许线程以更高的特权级别执行指令和操作，就像它在更高特权级别运行一样。由于更高特权级别通常可以访问额外的机器寄存器和其他状态，因此引入了 VCPU 对象作为此状态的存储。为简单起见，我们将此虚拟化的更高特权级别称为“客户模式”（guest mode）。VCPU 与 TCB 以一对一关系绑定，以便为线程提供以更高特权模式运行的能力。有关更精确的详细信息，请参阅 Arm 或 x86 部分。

VCPU 对象还具有额外的、架构特定的调用，用于操作额外的状态或硬件提供的其他虚拟化控制。将 VCPU 绑定到 TCB 仅通过对 VCPU 的调用来完成，而不是通过对 TCB。

提供的对象和调用一般来说是底层硬件原语和操作的最薄封装。因此，使用这些对象需要深入了解底层架构特定的硬件机制，描述中也假设读者具备此类知识。

6.4.1 Arm

当 TCB 具有绑定的 VCPU 时，它将可以访问（虚拟化的）系统寄存器、缓存和 TLB 维护指令，并能够自行处理一些异常。虚拟 GIC 将被启用，允许虚拟中断递送。

虚拟化的系统寄存器可以使用 seL4_ARM_VCPU_WriteRegs() 修改。通过分别配置 ARMv8 和 ARMv7 的 SPSR_EL1 或 cpsr 寄存器的模式部分，线程可以在客户内核模式下运行。

中断通过虚拟 GIC 虚拟化，需要使用 seL4_ARM_VCPU_InjectIRQ() 转发，该方法提供了一种管理虚拟 GIC 列表寄存器（List Register）的方式，列表寄存器是待递送给客户的中断队列。为了帮助管理该列表，虚拟 GIC 将发送 GIC 维护中断，这些中断作为 VGIC 维护故障（VGIC Maintenance Fault）递送。列表寄存器状态在 VCPU 上下文切换时保存和恢复，但目前没有手动执行此操作的方法。

共享外设中断（SPI）可以像普通 IRQ 一样处理并根据需要转发。虚拟私有外设中断（PPI）被捕获并作为 VPPI 事件故障递送，需要使用 seL4_ARM_VCPU_AckVPPI() 进行确认。

除上述异常和标准异常外，其他异常作为 VCPU 故障递送。

当内核支持虚拟化时，Stage 2 转换被启用。VCPU 将控制 Stage 1 转换，Stage 2 转换将用于系统的其余部分。由于 Stage 2 转换使用 VMID 而不是 ASID 来区分地址空间，因此将使用 VMID 来实现 seL4 ASID。实际上，这意味着在支持 16 位 VMID 之前，所有线程的 ASID 限制为 256。如果需要更多 ASID，ASID 将被动态重用，并伴随相关的缓存刷新和减速。

6.4.2 x86

具有绑定 VCPU 的 TCB 有两种执行模式：一种是原始线程，就像没有绑定的 VCPU 一样；另一种是使用 VCPU 的客户模式执行。从常规执行模式切换到客户执行模式通过使用 seL4_VMEnter() 系统调用完成。执行此系统调用会导致线程在此后每次被调度时，使用由 VCPU 控制的更高特权模式执行。如果客户执行模式生成任何类型的故障，或者如果消息到达 TCB 的绑定通知，TCB 将被切换回常规模式，seL4_VMEnter() 系统调用将返回一条指示返回原因的消息。

VCPU 状态和执行通过 seL4_VCPU_ReadVMCS() 和 seL4_VCPU_WriteVMCS() 调用控制。这些是硬件 vmread 和 vmwrite 指令的非常薄的封装，内核仅对参数进行足够的验证，以确保 VCPU 的配置不会以违反任何内核属性的方式运行。例如，不可能禁用外部中断退出（External Interrupt Exiting），因为这将阻止内核接收定时器中断并允许线程独占 CPU 时间。

客户执行模式的内存访问通过要求使用扩展页表（EPT，Extended Page Tables）来控制。存在一系列 EPT 相关的分页结构对象（EPTPML4、EPTPDPT、EPTPD、EPTPT），它们的操作方式与常规虚拟地址空间的对象完全相同。构建完成后，可以使用 seL4_TCB_SetEPTRoot() 为 TCB 提供一个 EPTPML4 作为 EPT 根，该根在客户模式下执行时充当 VSpace 根，而通过 seL4_TCB_SetSpace() 或 seL4_TCB_Configure() 设置的 VSpace 根在 TCB 以正常模式执行时继续提供转换。

可以通过 seL4_X86_VCPU_EnableIOPort() 调用将 I/O 端口的直接访问权限授予特权执行模式，并允许将提供的 I/O 端口能力链接到 VCPU，使其 I/O 端口范围的一个子集对 VCPU 可访问。链接意味着一个 I/O 端口能力只能在单个 seL4_X86_VCPU_EnableIOPort() 调用中使用，第二次调用将撤销前一次调用。链接还意味着如果 I/O 端口能力因任何原因被删除，该访问将相应地从 VCPU 中移除。

第 7 章 地址空间与虚拟内存

seL4 中的虚拟地址空间（virtual address space）称为 VSpace。与 CSpace（见第 3 章）类似，VSpace 由内核提供的对象组成。与 CSpace 不同，用于管理虚拟内存的对象与硬件对应，每种体系结构都定义了自己的分页结构对象类型。与 CSpace 的另一个不同之处是，我们仅将顶层分页结构称为 VSpace 对象。它提供了对 VSpace 的顶层权限。

所有体系结构通用的对象是 Frame（帧），表示一帧物理内存。Frame 对象通过 Page capability 进行操作，该 capability 既表示对帧的权限，也代表映射后的虚拟内存映射，即页面（page）。内核还提供 ASID Pool 对象和 ASID Control 调用，用于跟踪 VSpace 的地址空间标识符状态。

这些与 VSpace 相关的对象足以实现创建、操作和销毁虚拟内存地址空间所需的硬件数据结构。通常，虚拟内存空间的操作者需要对所需对象拥有适当的 capability。

7.1 对象

7.1.1 硬件虚拟内存对象

每种体系结构都有一个顶层分页结构（第 0 级）和若干中间级别。在泛指时，我们将这个顶层分页结构称为 VSpace 对象。实现 VSpace 对象的 seL4 对象类型取决于体系结构。例如，在 AArch32 上，VSpace 由 PageDirectory 对象表示，在 x64 上由 PML4 对象表示。

通常，每个级别的分页结构包含一些槽位，可以在其中映射下一级分页结构或一帧内存。分页结构的级别决定了帧的大小。每个级别的结构的大小和类型，以及该级别解析的虚拟地址位数，均由硬件定义。

seL4 内核提供了操作这些硬件分页结构的方法，包括映射和缓存操作。映射操作在被映射对象的 capability 上调用。例如，要在特定虚拟地址映射一个第 2 级分页结构，我们可以在第 2 级对象的 capability 上调用映射操作，并提供虚拟地址以及第 1 级对象的 capability 作为参数。

如果上一级（示例中的第 1 级）尚未被映射，映射操作将失败。开发者需要创建并映射所有分页结构，内核不会自动创建中间级别。

通常，VSpace 对象（顶层分页结构）没有映射调用，而是作为其他虚拟内存相关对象调用的参数使用。对于某些体系结构，VSpace 对象提供缓存操作调用。这允许更简单的策略选择：一个已委派 VSpace capability 的进程（例如在 AArch32 上的页目录）可以对该 capability 映射的所有帧执行缓存操作，而无需直接访问那些 capability。

本节其余部分详细介绍各体系结构的分页结构。

7.1.1.1 IA-32

在 IA-32 上，VSpace 对象由 PageDirectory 对象实现，它覆盖 32 位地址空间中的整个 4 GiB 范围，并构成顶层分页结构。二级页表（PageTable 对象）每个覆盖 4 MiB 范围。两个级别的结构均由虚拟地址中的 10 位进行索引。

7.1.1.2 x64

在 x86-64 上，VSpace 对象由 PML4 对象实现。定义了三个额外的分页结构级别，如下表所示。所有结构均由虚拟地址的 9 位进行索引。

7.1.1.3 AArch32

与 IA-32 类似，Arm AArch32 使用 PageDirectory 对象实现 VSpace 对象，覆盖整个 4 GiB 地址范围。AArch32 上的二级结构是 PageTable 对象。它们覆盖的地址范围取决于配置：标准配置为 1 MiB（20 位地址位），Hypervisor 配置为 2 MiB（21 位地址位）。

标准配置：

Hypervisor 配置：

7.1.1.4 AArch64

根据配置，Arm AArch64 处理器具有 3 级或 4 级页表结构。VSpace 对象是 seL4_ARM_VSpaceObject，这是一个用于顶层页表的独特对象类型。所有中间分页结构由虚拟地址的 9 位进行索引，并且都是 PageTable 对象。根据配置，顶层对象由 9 位或 10 位进行索引。宏 seL4_VSpaceIndexBits 以通用名称提供此值。下表显示了四级配置。

7.1.2 RISC-V

RISC-V 为所有级别提供相同的分页结构——PageTable。这意味着 VSpace 对象也由 PageTable 对象实现。

7.1.2.1 RISC-V 32-bit

32 位 RISC-V 的 PageTable 由虚拟地址的 10 位进行索引。

7.1.2.2 RISC-V 64-bit

64 位 RISC-V 遵循 SV39 模型，其中 PageTable 由虚拟地址的 9 位进行索引。虽然 RISC-V 允许多种不同的分页级别数量，但目前 seL4 仅支持恰好三级分页结构。

7.1.3 Page

Frame 对象通过 Page capability 使用，对应用于在虚拟地址空间中实现虚拟内存页面的物理内存帧。

Page 映射的虚拟地址必须与页面大小对齐，并且必须映射到合适的分页结构对象中，该分页结构对象本身必须已经被映射。

要以可读方式映射页面，对应的 Page capability 必须具有读权限。要以可写方式映射页面，capability 必须具有写权限。请求的映射权限通过类型为 seL4_CapRights 的参数在映射调用中指定。如果 capability 没有足够的权限来授权给定的映射，映射权限将被静默降级。具体的映射权限取决于体系结构，并在第 10 章中为每个函数进行了文档说明。在所有体系结构上，将页面映射为只写将导致该页面不可访问。

至少，每种体系结构为页面定义了 Map、Unmap 和 GetAddress 方法。各体系结构的页面 capability 调用可以在第 10 章找到，并按体系结构在下表中进行索引。

每种体系结构还定义了一系列页面大小。下一节展示可用的页面大小，以及映射级别（mapping level），指该页面必须映射到的分页结构级别。

7.1.3.1 AArch32 页面大小

节（section）和超级节（super section）的映射分别消耗页表和页目录中的 16 个槽位。

7.1.3.2 AArch64 页面大小

7.1.3.3 IA-32 页面大小

7.1.3.4 X64 页面大小

7.1.3.5 RISC-V 32-bit 页面大小

7.1.3.6 RISC-V 64-bit 页面大小

7.1.4 ASID Control

内核支持固定最大数量的地址空间标识符（ASID），该数量取决于体系结构。为了管理这一有限资源，seL4 提供了 ASID Control capability。ASID Control capability 可以与 Untyped capability 一起使用来创建 ASID Pool 对象和 capability，这些 capability 授权使用可用地址空间标识符的一个子集。ASID Control 对每种体系结构具有一个 MakePool 方法，列于下表中。

7.1.5 ASID Pool

ASID Pool 授予使用全局可用地址空间标识符子集的权利。该子集的大小取决于体系结构。要使 VSpace 对象可被线程使用，必须通过 ASID Pool capability 将其分配到一个 ASID。每个 ASID 最多可以分配给一个 VSpace。ASID Pool capability 对每种体系结构有一个调用——Assign。

7.2 映射属性

类型为 seL4_ARM_VMAttributes、seL4_x86_VMAttributes 或 seL4_RISCV_VMAttributes 的参数用于指定被映射页面的缓存行为。Arm 的可用值（可以进行按位或运算）如表 7.1 所示。IA-32 和 x64 的有效值枚举如表 7.2 所示。RISC-V 的可用值（可以进行按位或运算）如表 7.3 所示。映射属性可以使用 Map 调用和相同的虚拟地址在现有映射上进行更新。

表 7.1：Arm 页表项的虚拟内存属性。

表 7.2：x86 页表项的虚拟内存属性。

表 7.3：RISC-V 页表项的虚拟内存属性。

7.3 共享内存

seL4 内核不允许中间分页结构（例如 PageTable 对象）被共享，但允许页面在 VSpace 之间共享，以及 VSpace 在线程之间共享。

要共享一个页面，必须首先使用 seL4_CNode_Copy() 方法复制该 Page 的 capability，并将该副本用于将该页面映射到第二个地址空间的 Map 调用中（例如 seL4_ARM_Page_Map() 或 seL4_x86_Page_Map()）。尝试在不同的页表或地址空间中映射同一个 capability 两次将导致错误。

7.4 页面错误

页面错误（page fault）被报告给执行线程的异常处理器。参见第 6.2.7 节。

第 8 章 硬件 I/O

8.1 中断传递

中断（interrupt）以通知（notification）的形式传递。线程可以配置内核，使其在某个中断触发时向特定的 Notification 对象发送信号。线程随后可以通过在该 Notification 上调用 seL4_Wait() 或 seL4_Poll() 来等待中断发生。

IRQHandler capability 表示线程配置某个中断的能力。它们有三个方法：

• seL4_IRQHandler_SetNotification() 指定内核在中断发生时应向哪个 Notification 发送 signal()。驱动程序随后可以在此通知上调用 seL4_Wait() 或 seL4_Poll() 来等待中断到达。
• seL4_IRQHandler_Ack() 通知内核用户态驱动程序已完成中断处理，内核可以向应用程序发送更多待处理或新的中断。
• seL4_IRQHandler_Clear() 从 IRQHandler 对象中注销 Notification。

系统首次启动时，不存在任何 IRQHandler capability。相反，初始线程的 CSpace 包含一个 IRQControl capability。此 capability 可用于为系统中每个可用中断创建一个 IRQHandler capability。通常，系统的初始线程将确定系统中其他组件需要哪些 IRQ，为每个中断创建一个 IRQHandler capability，然后适当地委派生成的 capability。IRQControl 上的方法可用于为中断源创建 IRQHandler capability。

8.2 x86 特定的 I/O

8.2.1 中断

除了管理 IRQHandler capability 之外，x86 平台还需要配置 CPU 向量表中的传递位置。无论中断来自何处（IOAPIC、MSI 等），它都必须被分配一个唯一的传递向量，范围从 VECTOR_MIN 到 VECTOR_MAX。分配向量的权限通过 IRQControl capability 有效授予，可以视为内核将此命名空间的分配外包给用户态。

• seL4_IRQControl_GetIOAPIC() 为 IOAPIC 中断创建 IRQHandler capability
• seL4_IRQControl_GetMSI() 为 MSI 中断创建 IRQHandler capability

8.2.2 I/O 端口

在 x86 平台上，seL4 为用户态线程提供对 I/O 端口的访问。对 I/O 端口的访问由 IO Port capability 控制。每个 IO Port capability 标识可访问的端口范围。读取 I/O 端口通过 seL4_X86_IOPort_In8()、seL4_X86_IOPort_In16() 和 seL4_X86_IOPort_In32() 方法完成，允许读取 8 位、16 位和 32 位数据。类似地，写入 I/O 端口通过 seL4_X86_IOPort_Out8()、seL4_X86_IOPort_Out16() 和 seL4_X86_IOPort_Out32() 方法完成。每个方法接受一个 IO Port capability 和一个无符号整数端口作为参数，分别指示要读取或写入的 I/O 端口。在每种情况下，端口必须在给定 IO Port capability 标识的 I/O 端口范围内，方法才能成功。

I/O 端口方法在失败时返回错误码。如果在 IO Port capability 允许的范围之外尝试端口访问，将返回 seL4_IllegalOperation 错误码。由于读取 I/O 端口的调用需要返回两个值——读取的值和错误码——这些 API 调用返回一个包含 result 和 error 两个成员的结构体。

在系统初始化时，初始线程的 CSpace 包含 IOPortControl capability，可用于通过 seL4_X86_IOPort_Issue() 向 I/O 端口的子范围颁发 IO Port capability。任何颁发的范围不得与任何现有颁发的 IO Port capability 重叠。

8.2.3 I/O 空间

能够进行 DMA 的 I/O 设备带来安全风险，因为当设备访问内存时会绕过 CPU 的 MMU。在 seL4 中，设备驱动程序在用户空间运行，以将其排除在可信计算基之外。然而，恶意或有缺陷的设备驱动程序可能会编程设备访问或损坏不属于其地址空间的内存，从而破坏安全性。为了缓解这一威胁，seL4 在基于 Intel x86 的平台上提供了对 IOMMU 的支持。IOMMU 允许从设备的角度重新映射内存。它充当设备的 MMU，限制设备可以访问的系统内存区域。更多信息可以从 Intel 的 IOMMU 文档 [Intel Corporation, 2011¹⁶] 中获取。

内核提供了两个新对象来抽象 IOMMU：

• IOSpace：此对象表示与 PCI 总线上硬件设备关联的地址空间。它代表修改设备内存映射的权利。
• IOPageTable：此对象表示 IOMMU 硬件用于转换硬件内存访问的多级页表结构中的一个节点。

Page capability 用于表示映射到 I/O 地址空间中的实际帧。一个 Page 可以映射到 VSpace 或 IOSpace 中，但不能同时映射到两者。

IOSpace 和 VSpace 的错误处理方式有很大不同。VSpace 页面错误被重定向到线程的异常处理器（见第 6.2 节），异常处理器可以采取适当操作并在出错指令处重启线程。IOSpace 没有异常处理器的概念。相反，出错的事务会被简单地中止；设备驱动程序必须纠正错误原因并重试 DMA 事务。

初始线程的 CSpace 中提供了一个主 IOSpace capability。通过使用 seL4_CNode_Mint() 方法创建特定设备的 IOSpace capability，将设备的 PCI 标识符作为 badge 参数的低 16 位，Domain ID 作为 badge 参数的高 16 位。PCI 标识符在 PCI 规范 [Shanley and Anderson, 1999¹⁷] 中有完整说明，这里仅作简要描述。PCI 标识符是一个 16 位值。前 8 位标识设备所在的总线。接下来的 5 位是设备标识符：总线上的设备编号。最后 3 位是功能编号。单个设备可能由多个独立功能组成，每个功能可以通过 PCI 标识符寻址。Domain ID 在 Intel IOMMU 文档 [Intel Corporation, 2011¹⁶] 中有完整说明。目前没有方法向 seL4 查询 IOMMU 支持多少个 Domain ID，如果选择了不受支持的值，seL4_CNode_Mint() 方法将失败。

IOMMU 页表结构有三个级别。页表使用 seL4_X86_IOPageTable_Map() 方法映射到 IOSpace 中。此方法接受要映射的 IOPageTable、要映射到的 IOSpace 以及映射地址作为参数。在成功映射帧之前，必须映射三个级别的页表。帧使用 seL4_X86_Page_MapIO() 方法映射，其参数类似于将 Page 映射到 VSpace 的对应方法（见第 7 章），即 seL4_X86_Page_Map()。

取消映射通过常规的取消映射 API 调用完成（见第 7 章），即 seL4_X86_Page_Unmap()。

关于 seL4 的 IOMMU 抽象的更多信息可以在 [Palande, 2009¹⁸] 中找到。

8.3 Arm 特定的 I/O

8.3.1 Arm SMMU 2.0 版本

seL4 提供了一个用于编程 Arm 系统 MMU（SMMU）2.0 版本的 API，它允许系统软件管理可以发起直接内存访问（DMA）的设备的访问权限和地址转换。

Arm SMMU v2.0 实现允许设备内存事务与一个标识符（StreamID）关联，该标识符用于将事务引导通过 SMMU 转换上下文 bank（CB）。转换上下文 bank 可以执行地址转换、内存保护和内存属性转换。规范指定了不同类型的地址转换，对应 ArmV8 虚拟内存系统体系结构中的各个阶段，例如非安全 EL0、EL1 第一和第二阶段转换、Hyp 模式转换或安全模式转换。可以将不同的 StreamID 与同一个上下文 bank 关联，如果转换的阶段和类型相同，可以在上下文 bank 和软件 MMU 地址空间之间共享地址转换表。

当内存事务与 StreamID 或 CB 配置冲突时发生的错误相对于处理器元素的执行是异步的。发生这种情况时，使用中断允许 PE 处理 SMMU 错误。错误通过 SMMU 中的寄存器报告，可以在中断处理程序中查询。

当任何有效的页表映射条目发生更改时，需要执行 TLB 维护操作以保持 SMMU 转换缓存的一致性。

SMMU 实现通常有一个最大支持的 StreamID 数量。规范允许 StreamID 宽度最大为 16 位。还有固定数量的上下文 bank，最多 128 个。上下文 bank 可以是通用的或仅支持单个地址转换阶段。此信息由每个实现中的 ID 寄存器报告。

seL4 API 允许系统软件通过将 StreamID 分配到上下文 bank、将上下文 bank 绑定到页转换结构、实现 SMMU 错误处理以及执行显式 TLB 维护来管理 SMMU。这允许系统软件确保设备只能访问和修改已被明确授予访问权限的内存内容，并允许设备获得一个虚拟化的地址空间以执行 DMA。

所有 StreamID 和上下文 bank 都可以通过 capability 访问。控制 capability 用于创建引用系统中每个 StreamID 和上下文 bank 的 capability。内核使用两个静态 CNode 跟踪 StreamID 和上下文 bank 的分配，每种资源类型一个。这些 CNode 跟踪哪个 VSpace 绑定到上下文 bank，以及哪个上下文 bank 绑定到 StreamID。

这些 capability 允许用户线程实施访问控制策略。当 StreamID 或上下文 bank capability 被撤销时，内核将禁用上下文 bank 或 StreamID 映射。

TLB 维护由内核通过跟踪哪些上下文 bank 与特定 VSpace 关联来处理。内核在 VSpace 调用上执行的任何 TLB 维护操作也会应用到关联的上下文 bank。

SMMU 错误处理通过允许查询和清除每个上下文 bank 以及整个 SMMU 的错误状态的调用委派到用户态。SMMU 错误中断可以像其他平台级中断一样处理。

内核实现仅使用与内核为 VSpace 对象执行的转换相匹配的转换阶段。当 seL4 在 EL1 运行时，SMMU 仅使用阶段 1 转换（ASID），即在上下文 bank 属性配置中“阶段 1 搭配阶段 2 旁路”。当 Hypervisor 模式启用且 seL4 在 EL2 运行时，SMMU 仅执行阶段 2 转换。

四种 capability 类型提供对 SMMU 资源的访问：

• seL4_ARM_SID：授予访问单个事务流的 capability，可用于将流绑定和解绑到单个上下文 bank。
• seL4_ARM_CB：表示单个特定上下文 bank 的 capability。可用于绑定和解绑 VSpace 以分配上下文 bank 应使用的页表、分配 StreamID 和处理上下文 bank 错误。
• seL4_ARM_SIDControl：控制 capability，可用于创建指向特定事务流的 seL4_ARM_SID capability。seL4_ARM_SIDControl cap 用于管理 StreamID 配置的权限。此 capability 提供在初始线程的 CSpace 中。
• seL4_ARM_CBControl：控制 capability，可用于派生 seL4_ARM_CB capability。seL4_ARM_CBControl cap 用于管理上下文 bank 配置的权限。此 capability 提供在初始线程的 CSpace 中。

8.3.1.1 创建 seL4_ARM_SID capability

Arm SMMU 2.0 规范没有指定 StreamID 如何对应到不同设备。每个平台可以定义自己的 StreamID 分配策略。seL4_ARM_SIDControl capability 可用于为 SMMU 的任何有效 StreamID 创建 capability，并将访问权限委派给系统中的其他任务。

seL4_ARM_SIDControl_GetSID() 使用 seL4_ARM_SIDControl capability 创建一个新的 seL4_ARM_SID capability，表示单个 StreamID。此新 capability 被放置在提供的槽位中。期望控制 seL4_ARM_SIDControl capability 的线程了解系统中 StreamID 的分配方式。

Arm SMMU 2.0 规范描述了许多将 StreamID 与上下文 bank 关联的方式。目前仅支持 StreamID 到上下文 bank 的直接映射。

8.3.1.2 创建 seL4_ARM_CB capability

每个上下文 bank 允许 SMMU 维护一个活跃的转换上下文，带有自己的寄存器用于保存上下文特定信息。SMMU 有固定数量的可用上下文 bank，这些通过 seL4_ARM_CBControl capability 进行分配。

seL4_ARM_CBControl_GetCB() 使用 seL4_ARM_CBControl capability 创建一个新的 seL4_ARM_CB capability，表示单个上下文 bank。此新 capability 被放置在提供的槽位中。期望控制 seL4_ARM_CBControl capability 的线程了解每个索引引用的上下文 bank 的属性。

8.3.1.3 配置上下文 bank

通过提供 seL4_ARM_CB cap，用户态线程可以使用以下 API 配置 bank 使用的 VSpace：

• seL4_ARM_CB_AssignVspace() 配置上下文 bank 使用提供的 VSpace 根进行转换。
• seL4_ARM_CB_UnassignVspace() 移除已配置的 VSpace 并使 TLB 无效。

SMMU-v2 使用与 MMU 相同的分页结构（AArch64 和 AArch32 格式）。因此，不需要提供新的页结构 cap 集合，也不需要单独的映射和取消映射函数集。为了管理分配，内核有一个名为 smmuStateCBNode 的内部 CNode，存储执行上述 API 时创建的 VSpace_cap 副本。VSpace_cap 的副本包含其分配的 ContextBank 编号。因此，如果 VSpace_cap 被撤销，内核可以执行上下文 bank 失效操作。

8.3.1.4 配置流（事务）

用户态线程可以使用 seL4_ARM_SID capability 将上下文 bank 与以下方法绑定：

• seL4_ARM_SID_BindCB() 配置流使用给定的上下文 bank 进行转换。为简化过程，绑定还启用流 ID。seL4_ARM_SID_BindCB 在内核的内部 CNode 中生成 seL4_ARM_CB cap 的副本。这允许在 seL4_ARM_CB cap 被撤销时禁用流 ID。
• seL4_ARM_SID_UnbindCB() 从内核的内部 CNode 中移除 seL4_ARM_CB cap 并禁用流 ID。内核提供此 API 以便在多个 VSpace 之间共享流 ID。

如果流 ID 启用后出现任何异常，用户态软件应使用错误处理机制来解决它们。

8.3.1.5 复制和删除 cap

内核允许复制 ARM_SID cap 和 seL4_ARM_CB cap。这允许将 capability 委派给不同的线程。内核不允许复制 seL4_ARM_SIDControl 或 seL4_ARM_CBControl capability。

删除包含有效 capBindSID 字段的 seL4_ARM_CB cap 将：

• 使 StreamID 到 ContextBank 的分配在硬件上失效。

删除最后一个 seL4_ARM_CB cap 将：

• 执行 seL4_ARM_CB_UnassignVspace()，移除任何已配置的 VSpace，
• 使 TLB 无效。

类似地，删除包含已分配上下文 bank 编号的 VSpace_cap 将：

• 使上下文 bank 失效，
• 使 TLB 无效。

删除最后一个 ARM_SID cap 将：

• 执行 seL4_ARM_SID_UnbindCB()（删除已分配的 seL4_ARM_CB cap 的副本），
• 禁用流 ID。

8.3.1.6 TLB 失效

内核预计在 API 实现中执行所有必需的 SMMU TLB 维护操作。此外，内核提供了两个系统调用用于显式执行失效操作：

• seL4_ARM_CBControl_TLBInvalidateAll() 使所有上下文 bank 中的所有 TLB 条目失效。
• seL4_ARM_CB_TLBInvalidate() 使一个上下文 bank 中的所有 TLB 条目失效。

内核不对用户态应用程序如何使用 VSpace 施加任何限制，因此 VSpace 可以在普通线程和驱动程序之间共享。在线程和驱动程序之间共享 VSpace 也意味着在 CPU 核心中的 MMU 和设备事务使用的 SMMU 之间共享该 VSpace 中的所有映射。此外，SMMU 中的多个上下文 bank 可以共享一个 VSpace。因此，维护 MMU 中的 TLB 与 SMMU 上下文 bank 中的 TLB 之间的一致性非常重要。

内核通过维护以下信息来记录 VSpace 在 SMMU 上下文 bank 中的使用情况：使用给定 ASID 的上下文 bank 数量，以及给定上下文 bank 正在使用的 ASID。此设计背后有以下几个原因：

• 首先，ASID 是表示 VSpace 的高效方式。在 seL4 中，每个 VSpace 在准备使用之前被分配一个 ASID，并且该 ASID 在 VSpace 被删除之前不会更改。记录有多少上下文 bank 在使用 VSpace 的 ASID 等同于记录 VSpace 在上下文 bank 中的使用情况。
• 其次，所有 TLB 失效操作都需要了解 ASID。有两种类型的 TLB 失效操作：使用 ASID 使页表条目失效（由更新页表条目触发，例如取消映射页面），以及使 ASID 的所有映射失效（由删除 VSpace 触发）。
• 第三，内核可以在任何情况下轻松找到上下文 bank 的 ASID，这对于执行 TLB 失效请求或从上下文 bank 取消分配 VSpace 很有用。

通过了解有多少上下文 bank 在使用 ASID，内核可以在每次 TLB 失效操作中轻松检查，如果值不为零则调用 SMMU 中的 TLB 失效。在 SMMU 的 TLB 失效操作中，内核搜索使用该 ASID 的上下文 bank，并在这些上下文 bank 中执行 TLB 失效。

理想情况下，SMMU 与系统其余部分共享相同的 ASID 或 VMID 命名空间。这允许 SMMU 通过监听 TLB 广播消息来维护 TLB 一致性。这意味着在流 ID 启用时，上下文 bank 应配置正确的 ASID 或 VMID。对于阶段 1 转换这不是问题，因为有大量的 ASID 位，可以使用现有 API 将 ASID 分配给 VSpace 根。然而，阶段 2 中使用的 VMID 只有 8 位，内核按需分配它们，如果 VSpace 数量超过可用 ASID，可以回收 VSpace 的硬件 ASID 以供重用。虽然这在 VSpace 仅用于 MMU 时是可行的，但在有多个活跃上下文 bank 的情况下则不行。因此，SMMU 中的上下文 bank 无法配置正确的 VMID。目前，SMMU 驱动使用私有的 VMID 空间，并使用上下文 bank 编号作为对应的 VMID 编号。

8.3.1.7 错误处理

用于报告事务错误的 IRQ 数量取决于硬件。有两种错误类型：全局错误（一般配置和事务错误）或上下文 bank 错误。对于事务错误，SMMU 报告出错的流 ID。全局错误报告：

• 无效上下文错误
• 未识别流错误
• 流匹配冲突错误
• 未实现的上下文 bank 错误
• 未实现的上下文中断错误
• 配置访问错误
• 外部错误

每个上下文 bank 包含用于报告地址转换错误的寄存器，例如出错地址或权限错误。SMMU 驱动通过首先读取全局错误寄存器（一个状态寄存器和三个错误综合寄存器），然后读取相应的上下文 bank 错误寄存器来识别错误原因。注意，SMMU 报告出错的事务（流）ID，可用于识别其上下文 bank ID。

• 系统假设：SMMU 的 IRQ 处理程序和 seL4_ARM_SIDControl cap 的持有者（控制流 ID 分配）都是受信任的。
• SMMU 中断与其他 IRQ 的处理方式相同，即内核不特殊对待 SMMU IRQ，通过 IRQ 通知报告中断。
• 内核提供了读取全局错误寄存器的 API：seL4_ARM_SIDControl_GetFault()。由于 IRQ 通知只能通过 badge 传递信息，seL4_ARM_SIDControl cap 的持有者可以通过此 API 获取更多信息。
• 如果错误与事务相关，seL4_ARM_SIDControl cap 的持有者将通知相应流 ID cap 的持有者，后者还应拥有绑定到此事务的上下文 bank cap 的副本。
• 内核提供了读取上下文 bank 错误寄存器的 API：seL4_ARM_CB_CBGetFault()，由上下文 bank cap 持有者（seL4_ARM_CB cap 持有者）使用。
• 错误处理完成后，服务器可以调用 seL4_ARM_CB_CBClearFault() 清除上下文 bank 上的错误状态，并调用 seL4_ARM_SIDControl_ClearFault() 清除 SMMU 上的错误状态。

第 9 章 系统引导启动

9.1 初始线程的环境

seL4 内核为初始线程创建了一个最小引导环境，初始线程以优先级 seL4_MaxPrio 和最高控制优先级 seL4_MaxPrio 启动。此环境由初始线程的 TCB、CSpace 和 VSpace 组成，VSpace 包含承载用户态映像（初始线程的代码/数据）和 IPC 缓冲区的帧。

在 MCS 内核上，初始线程配置为时间片为 CONFIG_BOOT_THREAD_TIME_SLICE 毫秒的时间片轮转调度上下文。不使用 MCS 时，所有线程（包括初始线程）使用 CONFIG_TIMER_TICK_MS * CONFIG_TIME_SLICE 的时间片进行时间片轮转调度。

初始线程的 CSpace 恰好由一个 CNode 组成，该 CNode 包含初始线程自身资源以及所有可用全局资源的 capability。CNode 大小可以在编译时配置（默认为 2^12 个槽位），但守护区域（guard）总是选择为使 CNode 解析的位数恰好等于体系结构的位数（32 位或 64 位）。这意味着 CNode 的第一个槽位的 CPtr 为 0x0，第二个槽位的 CPtr 为 0x1，以此类推。

前 15 个槽位（如果不使用 MCS 则为 14 个槽位）包含特定的 capability，如表 9.1 所列。

9.2 BootInfo 帧

CPtr 为 seL4_NumInitialCaps（在 seL4 用户态库中定义）及以上的 CNode 槽位在引导启动期间被动态填充。其确切内容取决于用户态映像大小、平台配置（设备）等。为了告诉初始线程哪些 capability 存储在其 CNode 中的什么位置，内核提供了一个 BootInfo 帧，该帧被映射到初始线程的地址空间中。映射地址由内核选择，并通过 CPU 寄存器传递给初始线程。

BootInfo 帧包含表 9.2 中描述的 C 结构体。它在 seL4 用户态库中定义。除了描述 capability 之外，它还告知初始线程当前平台的配置。

seL4_SlotRegion 类型是一个 C 结构体，包含 start 和 end 槽位 CPtr。它表示初始线程 CNode 中一个槽位区域，以 CPtr start 开始，end 为区域结束后的第一个槽位的 CPtr，即 end - 1 指向区域的最后一个槽位。

固定 BootInfo 帧的大小为 seL4_BootInfoFrameSize。在标准配置中，这是一个页面，在 x86、ARM 和 RISC-V 上为 4 KiB。根据体系结构和平台的不同，其后可能跟随额外的可变引导信息。

表 9.1：初始线程的 CNode 内容。

此数据的总体大小为 extraLen，它包含一系列数据块（blob），每个数据块以表 9.3 中描述的 seL4_BootInfoHeader 开头。此头部描述了数据块的内容和长度，其中长度包含头部本身。因此，长度可用于跳过未知的块。唯一通用定义的块类型是 SEL4_BOOTINFO_HEADER_PADDING，描述一个仅用于填充的数据块。extraBIPages 槽位区域给出了组成额外引导信息区域的页面帧 capability。

userImageFrames 中的 capability 按顺序排列，第一个 capability 引用用户态映像的第一帧，以此类推。userImagePaging 中的 capability 按分页结构大小的降序排列。在给定的分页结构大小内，capability 按对应对象映射到初始线程地址空间的虚拟地址排列。

由用户态推断 userImageFrames 中 capability 引用的帧的虚拟地址以及 userImagePaging 中 capability 引用的分页结构的虚拟地址和类型。用户态通常有办法找出其代码和数据映射到的虚拟地址（例如，在 GCC 中，使用标准链接器脚本时，可以使用 __executable_start 和 _end 符号）。此外，初始线程可以假设其地址空间是虚拟连续的，并由体系结构上可用的最小帧组成。还假设初始线程知道其运行的体系结构上有哪些分页结构可用。这些信息，结合对 userImageFrames 和 userImagePaging 中 capability 排列方式的了解，为用户态推断每个帧 capability 的虚拟地址以及每个分页结构 capability 的虚拟地址和类型提供了足够的信息。

非类型化内存（untyped memory）以无特定顺序给出。数组条目 untypedList[i] 存储槽位区域 untyped 中第 i 个非类型化 cap 的非类型化内存信息。因此，数组长度至少为 untyped.end - untyped.start。实际长度在内核中硬编码，与数组的读取者无关。非类型化内存信息存储在 seL4_UntypedDesc 结构体中（如表 9.4 所述），详细描述了非类型化支持的内存的地址、大小和类型。这允许用户态推断重类型化帧的物理内存地址，并在没有 IOMMU 可用时使用它们启动 DMA 传输。内核不保证特定大小的非类型化内存一定可用。

如果平台有 seL4 支持的 IOMMU，numIOPTLevels 包含 IOMMU 页表级别的数量。用户态在构建 IOMMU 地址空间（IOSpace）时需要此信息。如果没有 IOMMU 支持，numIOPTLevels 为 0。

在 Arm 上，如果平台有任何可用的 SMMU 单元，它们的 capability 将由 ioSpaceCaps 槽位区域描述。从此区域中的 capability 到特定 SMMU 的映射是平台特定的。

表 9.2：BootInfo 结构体。

表 9.3：BootInfoHeader 结构体。

9.3 引导命令行参数

在 IA-32 上，seL4 接受引导命令行参数，这些参数通过兼容 multiboot 的引导加载程序（例如 GRUB、syslinux）传递给内核。多个参数以空格分隔。接受两种形式的参数：(1) 形式为 “key=value” 的键值参数，(2) 形式为 “key” 的单独键。键值形式的 value 字段可以是字符串、十进制整数、以 “0x” 开头的十六进制整数，或整数列表（列表元素以逗号分隔）。键和值中不能有任何空格，“=” 或逗号前后也不能有空格。参数及其默认值（如果未指定）列于表 9.5 中。

表 9.4：seL4_UntypedDesc 结构体。

表 9.5：IA-32 引导命令行参数。

第10章 seL4 API 参考

10.1 错误码

使用无效参数调用能力将导致错误。seL4 系统调用在消息标签中返回错误码，并在消息寄存器中返回简短的错误描述，以帮助程序员确定错误原因。

10.1.1 无效参数

非能力参数无效。

10.1.2 无效能力

能力参数无效。

10.1.3 非法操作

请求的操作不被允许。

10.1.4 范围错误

参数超出允许范围。

10.1.5 对齐错误

提供的参数不满足对齐要求。

10.1.6 查找失败

无法查找能力。

10.1.7 截断消息

消息中发送的消息字或能力过少。

10.1.8 先删除

系统调用参数中指定的目标槽已被占用。

10.1.9 先撤销

该对象当前有其他对象派生自它，在删除这些对象或对该能力执行撤销调用之前，无法执行所请求的调用。

10.1.10 内存不足

Untyped Memory 对象没有足够的未分配空间来完成 seL4_Untyped_Retype() 请求。

10.2 系统调用

10.2.1 通用系统调用

本节提供非 MCS 内核配置的系统调用 API。

10.2.1.1 Send

LIBSEL4_INLINE_FUNC void seL4_Send

向能力发送消息。

返回值：此方法不返回任何内容。

描述：参见第 2.2 节

10.2.1.2 Recv

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv

阻塞直到在端点上收到消息。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：参见第 2.2 节

10.2.1.3 Call

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Call

调用能力。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：参见第 2.2 节

10.2.1.4 Reply

LIBSEL4_INLINE_FUNC void seL4_Reply

对线程上次被调用时存储的一次性回复能力执行发送。如果没有回复能力（这可能发生在被阻塞的线程通过销毁等操作被解除阻塞时），则不执行任何操作。

返回值：此方法不返回任何内容。

描述：参见第 2.2 节

10.2.1.5 非阻塞发送

LIBSEL4_INLINE_FUNC void seL4_NBSend

对能力执行非阻塞发送。

返回值：此方法不返回任何内容。

描述：参见第 2.2 节

10.2.1.6 回复接收

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv

在一个系统调用中执行回复后跟接收。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：参见第 2.2 节

10.2.1.7 非阻塞接收

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv

从端点接收消息，但在没有待处理消息时不阻塞。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：参见第 2.2 节

10.2.1.8 Yield

LIBSEL4_INLINE_FUNC void seL4_Yield

将剩余时间片捐献给同优先级的线程。

返回值：此方法不返回任何内容。

描述：参见第 2.2 节

10.2.1.9 Signal

LIBSEL4_INLINE_FUNC void seL4_Signal

信号通知。

返回值：此方法不返回任何内容。

描述：这不是内核识别的正式系统调用，而是一个便捷封装，调用 seL4_Send()。它对于信号通知很有用。参见第 2.2 节中 seL4_Send() 的描述。

10.2.1.10 Wait

LIBSEL4_INLINE_FUNC void seL4_Wait

对通知对象执行接收。

返回值：此方法不返回任何内容。

描述：这不是内核识别的正式系统调用，而是一个便捷封装，调用 seL4_Recv()。参见第 2.2 节中 seL4_Recv() 的描述。

10.2.1.11 Poll

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Poll

对通知对象执行非阻塞接收。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：这不是内核识别的正式系统调用，而是一个便捷封装，调用 seL4_NBRecv()。它用于对通知执行非阻塞等待。参见第 2.2 节中 seL4_NBRecv() 的描述。

10.2.2 通用系统调用 (MCS)

本节提供 MCS 内核配置的系统调用 API。

10.2.2.1 Send

LIBSEL4_INLINE_FUNC void seL4_Send

向能力发送消息。

返回值：此方法不返回任何内容。

描述：参见第 2.2 节

10.2.2.2 Recv

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv

阻塞直到在端点上收到消息。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：参见第 2.2 节

10.2.2.3 Call

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Call

调用能力。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：参见第 2.2 节

10.2.2.4 非阻塞发送

LIBSEL4_INLINE_FUNC void seL4_NBSend

对能力执行非阻塞发送。

返回值：此方法不返回任何内容。

描述：参见第 2.2 节

10.2.2.5 回复接收

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv

在一个系统调用中执行回复后跟接收。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：参见第 2.2 节

10.2.2.6 非阻塞接收

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv

从端点接收消息，但在没有待处理消息时不阻塞。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：参见第 2.2 节

10.2.2.7 非阻塞发送接收

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecv

在一个系统调用中对一个能力执行非阻塞发送，对另一个能力执行阻塞接收。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：参见第 2.2 节

10.2.2.8 非阻塞发送等待

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWait

在一个系统调用中非阻塞调用一个能力并等待另一个能力。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：参见第 2.2 节

10.2.2.9 Yield

LIBSEL4_INLINE_FUNC void seL4_Yield

让出剩余时间片。周期线程在下次零星补充之前不会被再次调度。

返回值：此方法不返回任何内容。

描述：参见第 2.2 节

10.2.2.10 Wait

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Wait

对端点或通知对象执行等待。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：在通知或端点上阻塞等待消息。Wait 不需要回复对象。Wait 不应与 Call 配对使用，因为它不提供回复对象。如果 Wait 与 Call 配对，等待者在接收消息后将阻塞。参见第 2.2 节中 seL4_Wait() 的描述。

10.2.2.11 非阻塞等待

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBWait

对端点或通知对象执行轮询等待。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：轮询通知或端点等待消息。Wait 不需要回复对象。Wait 不应与 Call 配对使用。参见第 2.2 节中 seL4_NBWait() 的描述。

10.2.2.12 Poll

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Poll

对通知对象执行非阻塞接收。

返回值：如第 4.1 节所述的 seL4_MessageInfo_t 结构

描述：这不是内核识别的正式系统调用，而是一个便捷封装，调用 seL4_NBWait()。它用于对通知执行非阻塞等待。参见第 2.2 节中 seL4_NBWait() 的描述。

10.2.2.13 Signal

LIBSEL4_INLINE_FUNC void seL4_Signal

信号通知。

返回值：此方法不返回任何内容。

描述：这不是内核识别的正式系统调用，而是一个便捷封装，调用 seL4_Send()。它对于信号通知很有用。参见第 2.2 节中 seL4_Send() 的描述。

10.2.3 调试系统调用

本节记录了内核使用 DEBUG_BUILD 配置构建时可用的调试系统调用。对于依赖内核串口驱动的系统调用，还必须启用 PRINTING。

10.2.3.1 输出字符

LIBSEL4_INLINE_FUNC void seL4_DebugPutChar

通过内核输出单个字符。

返回值：此方法不返回任何内容。

描述：使用内核串口驱动输出单个字符。当用户级串口驱动不可用时，这对于调试很有用。

10.2.3.2 转储调度器

LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler

输出内核调度器的内容。

返回值：此方法不返回任何内容。

描述：将所有 TCB 对象的状态转储到内核串口输出。此系统调用将输出包含以下内容的表格：

• Address：该线程的 TCB 对象地址
• Name：线程的名称（如果已设置）
• IP：线程当前的指令指针内容
• Priority：该线程的优先级
• State：线程的状态

10.2.3.3 停机

LIBSEL4_INLINE_FUNC void seL4_DebugHalt

停机系统。

返回值：此方法不返回任何内容。

描述：此调试系统调用将导致内核立即停止响应系统调用。内核将永久切换到禁用中断的空闲线程。根据平台不同，内核可能会将硬件切换到低功耗状态。

10.2.3.4 快照

LIBSEL4_INLINE_FUNC void seL4_DebugSnapshot

输出当前内核状态的 capDL 转储。

返回值：此方法不返回任何内容。

描述：此调试系统调用将使用 capDL 输出当前内核中的所有能力。

10.2.3.5 能力标识

LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify

标识当前 CSpace 中能力的类型。

返回值：传入的能力的类型。

描述：此调试系统调用返回当前 CSpace 中能力槽中能力的类型。返回的类型不是 libsel4 类型，而是指内部 seL4 类型。这可以在已构建的内核中查找（生成的）enum cap_tag，类型 cap_tag_t 来确定。

10.2.3.6 命名线程

LIBSEL4_INLINE_FUNC void seL4_DebugNameThread

命名线程。

返回值：此方法不返回任何内容。

描述：命名线程。此名称随后将在所有调试输出中由内核输出。注意，可以传递给此函数的最大名称长度受限于 IPC 消息中能容纳的字符数（seL4_MsgMaxLength 乘以一个字中能容纳的字符数）。但名称也会被截断以适应 TCB 对象。对于某些平台，可能需要在调试构建中将 seL4_TCBBits 增加 1 以容纳足够长的名称。

10.2.3.7 发送 SGI 0-15

LIBSEL4_INLINE_FUNC void seL4_DebugSendIPI

发送任意 SGI。

返回值：此方法不返回任何内容。

描述：向指定目标核心发送任意 SGI（核心特定中断 0-15）。

10.2.3.8 运行

LIBSEL4_INLINE_FUNC void seL4_DebugRun

在内核模式下运行用户级函数。

返回值：此方法不返回任何内容。

描述：此极其危险的函数用于从用户级运行需要在内核模式下执行的基准测试和调试代码。它不应在发布版内核中使用。这之所以可行，是因为内核可以访问设备内存的所有用户映射，并且在内核入口时不切换页目录。与本节中其他系统调用不同，seL4_DebugRun 不依赖于 DEBUG_BUILD 配置选项，而是依赖于其自己的配置变量 DANGEROUS_CODE_INJECTION。

10.2.4 基准测试系统调用

本节记录了内核配置启用基准测试时可用的系统调用。在构建内核时可以配置几种不同的基准测试模式：

1. BENCHMARK_TRACEPOINTS：在内核和计时代码中启用跟踪点。
2. BENCHMARK_TRACK_KERNEL_ENTRIES：跟踪内核入口的信息。
3. BENCHMARK_TRACK_UTILISATION：允许用户获取系统、线程和/或空闲线程的 CPU 时间信息。

10.2.4.1 重置日志

LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkResetLog

重置基准测试日志。

返回值：如果用户级日志缓冲区尚未由用户设置，则返回 seL4_Error 错误（BENCHMARK_TRACEPOINTS/BENCHMARK_TRACK_KERNEL_ENTRIES）。

描述：此系统调用的行为取决于调用此系统调用时的基准测试模式：

1. BENCHMARK_TRACEPOINTS：将日志索引重置为 0，
2. BENCHMARK_TRACK_KERNEL_ENTRIES：同上，
3. BENCHMARK_TRACK_UTILISATION：重置基准测试和当前线程开始时间（为调用此系统调用的时间），将空闲线程利用率重置为 0，并开始跟踪利用率。

10.2.4.2 终结日志

LIBSEL4_INLINE_FUNC seL4_Word seL4_BenchmarkFinalizeLog

停止基准测试日志。

返回值：日志缓冲区中最终条目的索引（如果启用了 BENCHMARK_TRACEPOINTS/BENCHMARK_TRACK_KERNEL_ENTRIES）。

描述：此系统调用的行为取决于调用此系统调用时的基准测试模式：

1. BENCHMARK_TRACEPOINTS：将最终日志缓冲区索引设置为当前索引，
2. BENCHMARK_TRACK_KERNEL_ENTRIES：同上，
3. BENCHMARK_TRACK_UTILISATION：将基准测试结束时间设置为当前时间，停止跟踪利用率。

10.2.4.3 设置日志缓冲区

LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkSetLogBuffer

设置日志缓冲区。

返回值：如果 frame_cptr 无效且无法设置缓冲区，则返回 seL4_IllegalOperation 错误。

描述：提供一个大帧对象供内核用作日志缓冲区。该对象不能是设备内存，大小必须为 seL4_LargePageBits。

10.2.4.4 空系统调用

LIBSEL4_INLINE_FUNC void seL4_BenchmarkNullSyscall

立即进出内核的空系统调用，用于微基准测试中计时内核陷阱。

返回值：此方法不返回任何内容。

描述：用于计时内核陷阱（进入和退出）。

10.2.4.5 刷新缓存

LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushCaches

刷新硬件缓存。

返回值：此方法不返回任何内容。

描述：刷新此平台的所有可能的硬件缓存。

10.2.4.6 刷新 L1 缓存

LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushL1Caches

刷新 L1 缓存。

返回值：此方法不返回任何内容。

描述：刷新此平台的 L1 缓存（目前仅支持 ARM）。允许指定要刷新的缓存类型（即仅指令缓存、仅数据缓存以及指令缓存和数据缓存两者）。

10.2.4.7 获取线程利用率

LIBSEL4_INLINE_FUNC void seL4_BenchmarkGetThreadUtilisation

获取利用率计时信息。

返回值：此方法不返回任何内容。

描述：获取系统、请求的线程和空闲线程的计时信息。此类信息写入调用者的 IPC 缓冲区；参见 benchmark_track_util_ipc_index 枚举的定义以获取 IPC 缓冲区上返回的数据/格式的更多详细信息。

10.2.4.8 重置线程利用率

LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation

重置特定线程的利用率计时。

返回值：此方法不返回任何内容。

描述：重置特定线程的内核计时信息数据（开始时间和利用率）。

10.2.4.9 转储所有线程利用率

LIBSEL4_INLINE_FUNC void seL4_BenchmarkDumpAllThreadsUtilisation

打印当前节点上每个线程的当前累计周期计数。

返回值：此方法不返回任何内容。

描述：使用内核的 printf 以以下格式在每行打印周期数：thread_name,thread_cycles

10.2.4.10 重置所有线程利用率

LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetAllThreadsUtilisation

重置当前节点上每个线程的累计周期计数。

返回值：此方法不返回任何内容。

描述：将每个线程的周期计数重置为 0。

10.2.5 x86 系统调用

10.2.5.1 VMEnter

LIBSEL4_INLINE_FUNC seL4_Word seL4_VMEnter

将当前线程切换为从其绑定的 VCPU 执行。

返回值：SEL4_VMENTER_RESULT_NOTIF（如果收到通知）或 SEL4_VMENTER_RESULT_FAULT（如果客户模式执行因任何原因发生故障）

描述：将当前线程的执行模式从正常 TCB 执行切换为使用其绑定 VCPU 的客户执行。有关 VCPU 和执行模式的详细信息，参见第 6.4 节。

调用 seL4_VMEnter 类似于回复故障，因为可以在消息中提供寄存器更新，但与故障不同的是，不发送消息信息（参见第 4.1 节），因为寄存器不是可选的，必须发送的数量是固定的。硬件寄存器到消息寄存器的映射为：

• SEL4_VMENTER_CALL_EIP_MR 在客户模式下开始执行指令的地址
• SEL4_VMENTER_CALL_CONTROL_PPC_MR 基于主处理器的 VM 执行控制的新值
• SEL4_VMENTER_CALL_CONTROL_ENTRY_MR VM 入口控制的新值

返回时，这三个相同的消息寄存器将被填充为特权模式停止执行时的值。如果此函数返回 SEL4_VMENTER_RESULT_FAULT，则将填充以下额外的消息寄存器：

• SEL4_VMENTER_FAULT_REASON_MR
• SEL4_VMENTER_FAULT_QUALIFICATION_MR
• SEL4_VMENTER_FAULT_INSTRUCTION_LEN_MR
• SEL4_VMENTER_FAULT_GUEST_PHYSICAL_MR
• SEL4_VMENTER_FAULT_RFLAGS_MR
• SEL4_VMENTER_FAULT_GUEST_INT_MR
• SEL4_VMENTER_FAULT_CR3_MR
• SEL4_VMENTER_FAULT_EAX
• SEL4_VMENTER_FAULT_EBX
• SEL4_VMENTER_FAULT_ECX
• SEL4_VMENTER_FAULT_EDX
• SEL4_VMENTER_FAULT_ESI
• SEL4_VMENTER_FAULT_EDI
• SEL4_VMENTER_FAULT_EBP

10.3 架构无关的对象方法

10.3.1 seL4_CNode

10.3.1.1 取消带徽章发送

static inline int seL4_CNode_CancelBadgedSends

取消带徽章发送方法旨在允许权威方重用徽章。当与带徽章的端点能力一起使用时，它将取消该端点和徽章的所有未完成发送操作。此操作对无徽章能力或其他对象无效。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 3.1.2 节。

10.3.1.2 Copy

static inline int seL4_CNode_Copy

复制能力，同时设置其访问权限

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 3.1.2 节。

10.3.1.3 Delete

static inline int seL4_CNode_Delete

删除能力

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 3.1.2 节。

10.3.1.4 Mint

static inline int seL4_CNode_Mint

复制能力，同时设置其访问权限和徽章

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 3.1.2 节。

10.3.1.5 Move

static inline int seL4_CNode_Move

移动能力

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 3.1.2 节。

10.3.1.6 Mutate

static inline int seL4_CNode_Mutate

移动能力，同时设置其保护。此操作主要用于设置 CNode 能力的保护而不丢失该 CNode 能力的可撤销性。所有其他用途可以用 Mint 和 Delete 的组合替代。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 3.1.2 节。

10.3.1.7 Revoke

static inline int seL4_CNode_Revoke

删除能力的所有子能力

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 3.1.2 节。

10.3.1.8 Rotate

static inline int seL4_CNode_Rotate

给定 3 个能力槽——目标、枢轴和源——将枢轴槽中的能力移动到目标槽，将源槽中的能力移动到枢轴槽

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 3.1.2 节。

10.3.1.9 保存调用者

static inline int seL4_CNode_SaveCaller

将线程上次被调用时的回复能力保存在给定的 CSpace 中，以便稍后调用

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 3.1.2 节。

10.3.2 seL4_DomainSet

10.3.2.1 Set

static inline int seL4_DomainSet_Set

更改线程的域。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.3 节。

10.3.3 seL4_IRQControl

10.3.3.1 获取 IRQ 处理程序

static inline int seL4_IRQControl_Get

创建 IRQ 处理程序能力

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.1 节。

10.3.4 seL4_IRQHandler

10.3.4.1 确认

static inline int seL4_IRQHandler_Ack

确认中断的接收并重新启用它

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.1 节。

10.3.4.2 清除

static inline int seL4_IRQHandler_Clear

从 IRQ 槽清除处理程序能力

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.1 节。

10.3.4.3 设置通知

static inline int seL4_IRQHandler_SetNotification

设置内核在所提供 IRQ 处理程序能力控制的中断上将信号通知的通知

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.1 节。

10.3.5 seL4_SchedContext (MCS)

10.3.5.1 Bind

static inline int seL4_SchedContext_Bind

将对象绑定到调度上下文。对象可以是通知对象或线程。如果对象是线程且线程处于可运行状态且调度上下文有可用预算，这将启动线程运行。如果对象是通知，当被动线程在通知对象上等待且信号到达时，被动线程将接收调度上下文并持有它直到再次在通知对象上等待。如果调度上下文已经绑定到通知对象，此操作对通知对象将失败；如果调度上下文已经绑定到线程，此操作对线程对象将失败。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1 节

10.3.5.2 Consumed

static inline seL4_SchedContext_Consumed_t seL4_SchedContext_Consumed

返回自上次调用此函数或触发超时异常以来此调度上下文使用的时间量

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1 节

10.3.5.3 解绑对象

static inline int seL4_SchedContext_UnbindObject

将对象从调度上下文解绑。对象可以是线程或通知。如果被解绑的线程是绑定到此调度上下文的线程，这将使线程变为被动。然而，如果被解绑的线程通过 IPC 上的调度上下文捐赠接收到调度上下文，调度上下文将归还给最初绑定到的线程。如果对象是通知且绑定到调度上下文，则解绑它。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1.8 节

10.3.5.4 Unbind

static inline int seL4_SchedContext_Unbind

将任何对象（线程或通知对象）从调度上下文解绑。这将使绑定的线程变为被动，参见第 6.1.5 节。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1 节

10.3.5.5 YieldTo

static inline seL4_SchedContext_YieldTo_t seL4_SchedContext_YieldTo

如果线程当前可运行且运行在此调度上下文上，且调度上下文有可用预算，将其放在调度队列头部。如果调用者与线程优先级相同，这将导致线程被调度。如果调用者优先级更高，线程将不会运行直到该线程优先级成为系统中最高优先级。调用者必须具有大于或等于线程优先级的最大控制优先级。

返回值：参见第 6.1.7 节

描述：正在操作的调度上下文的能力。

10.3.6 seL4_SchedControl (MCS)

10.3.6.1 配置标志

static inline int seL4_SchedControl_ConfigureFlags

通过调用调度控制能力来设置调度上下文的参数。如果调度上下文绑定到当前正在运行的线程，参数将立即生效：即当前预算将增加或减少新预算与先前预算之间的差额，补充时间将根据周期中的任何差异进行更新。这可能导致活动线程被推迟或释放，具体取决于参数更改的性质和线程的状态。此外，如果调度上下文之前为空（无预算）但绑定到可运行线程，这可能导致线程首次运行，因为它现在可以访问 CPU 时间。如果参数太小（小于此平台的内核 WCET）或太大（将导致计时器溢出），此调用将返回 seL4_InvalidArgument。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1 节

10.3.7 seL4_TCB

10.3.7.1 绑定通知

static inline int seL4_TCB_BindNotification

将通知对象绑定到 TCB

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 5.3 节

10.3.7.2 配置单步执行

static inline seL4_TCB_ConfigureSingleStepping_t seL4_TCB_ConfigureSingleStepping

设置或修改目标 TCB 的单步执行选项。后续对此函数的调用将覆盖先前的配置。根据处理器架构，这可能会也可能不会消耗硬件寄存器。

返回值：seL4_TCB_ConfigureSingleStepping_t：包含 seL4_Error error（seL4 API 错误值）和 seL4_Bool bp_was_consumed（布尔值，指示传递给函数的 bp_num 断点 ID 是否被消耗在单步执行功能的设置中：如果为 true，调用者不应尝试重用 bp_num，直到通过后续调用 seL4_TCB_ConfigureSingleStepping 并将 num_instructions 参数设为 0 来禁用单步执行功能）。

描述：参见第 6.2.5 节和第 6.2.4 节

10.3.7.3 Configure

static inline int seL4_TCB_Configure

设置 TCB 的参数

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1 节

10.3.7.4 复制寄存器

static inline int seL4_TCB_CopyRegisters

将寄存器从一个线程复制到另一个线程

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：在此函数的上下文中，帧寄存器是被系统调用读取、修改或保留的寄存器，整数寄存器是不被系统调用读取、修改或保留的寄存器。具体细节请参阅 seL4 用户空间库源代码。参见第 6.1.3 节

10.3.7.5 获取断点

static inline seL4_TCB_GetBreakpoint_t seL4_TCB_GetBreakpoint

读取断点或观察点的当前配置。

返回值：seL4_TCB_GetBreakpoint_t：包含 seL4_Error error（seL4 API 错误值）、seL4_Word vaddr（断点当前将被触发的虚拟地址）、seL4_Word type（当前将触发断点的操作类型，是指令执行还是数据访问）、seL4_Word size（断点跨度大小的整数值，通常是 2 的幂（1、2、4 等））、seL4_Word rw（当前将触发断点的访问方向，是读、写还是两者）和 seL4_Bool is_enabled（指示在满足匹配条件时断点当前是否会被触发）。

描述：参见第 6.2.4 节

10.3.7.6 读取寄存器

static inline int seL4_TCB_ReadRegisters

将线程的寄存器读入给定 seL4_UserContext 的前 count 个字段

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1.13 节

10.3.7.7 Resume

static inline int seL4_TCB_Resume

恢复线程

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1.3 节

10.3.7.8 设置断点

static inline int seL4_TCB_SetBreakpoint

设置或修改线程的断点或观察点。对此函数的调用将覆盖目标断点的先前配置。不要将此与 seL4_SingleStep 一起使用：API 将拒绝调用并返回错误。相反，使用 seL4_TCB_ConfigureSingleStepping 来配置单步执行。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.2.4 节

10.3.7.9 设置 CPU 亲和性

static inline int seL4_TCB_SetAffinity

在多核机器中更改线程的当前 CPU

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1.2 节

10.3.7.10 设置 IPC 缓冲区

static inline int seL4_TCB_SetIPCBuffer

设置线程的 IPC 缓冲区

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1 节和第 4.1 节

10.3.7.11 设置最大控制优先级

static inline int seL4_TCB_SetMCPriority

更改线程的最大控制优先级

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1.5 节

10.3.7.12 设置优先级

static inline int seL4_TCB_SetPriority

更改线程的优先级

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1.5 节

10.3.7.13 设置调度参数

static inline int seL4_TCB_SetSchedParams

更改线程的优先级和最大控制优先级。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1.5 节

10.3.7.14 SetSpace

static inline int seL4_TCB_SetSpace

设置线程的故障端点、CSpace 和 VSpace

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1 节

10.3.7.15 设置 TLS 基址

static inline int seL4_TCB_SetTLSBase

设置目标 TCB 的 TLS 基址。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：用于设置线程本地存储 (TLS) 基址的调用。这确保在所有平台上，TLSBase 寄存器被视为完全可变的，就像所有通用寄存器一样，即使是在修改为特权操作的平台上。

10.3.7.16 Suspend

static inline int seL4_TCB_Suspend

挂起线程

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1.3 节

10.3.7.17 解绑通知

static inline int seL4_TCB_UnbindNotification

从 TCB 解绑任何通知对象

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 5.3 节

10.3.7.18 取消断点

static inline int seL4_TCB_UnsetBreakpoint

禁用硬件断点或观察点。调用者应假定硬件寄存器的底层配置也已被清除。不要使用此方法清除单步执行：API 将拒绝调用并返回错误。相反，使用 seL4_TCB_ConfigureSingleStepping 来禁用单步执行。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.2.4 节

10.3.7.19 写入寄存器

static inline int seL4_TCB_WriteRegisters

将线程的寄存器设置为给定 seL4_UserContext 的前 count 个字段

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1.13 节

10.3.8 seL4_TCB (MCS)

10.3.8.1 Configure (MCS)

static inline int seL4_TCB_Configure

设置 TCB 的参数

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1 节

10.3.8.2 设置调度参数 (MCS)

static inline int seL4_TCB_SetSchedParams

更改线程的优先级、最大控制优先级、调度上下文和故障处理程序。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1.5 节

10.3.8.3 SetSpace (MCS)

static inline int seL4_TCB_SetSpace

设置线程的故障端点、CSpace 和 VSpace

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.1 节

10.3.8.4 设置超时端点

static inline int seL4_TCB_SetTimeoutEndpoint

设置线程的超时端点。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：如果超时端点不是空能力，超时异常消息将传递到此端点。

10.3.9 seL4_Untyped

10.3.9.1 Retype

static inline int seL4_Untyped_Retype

重类型化 untyped 对象

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：给定一个 untyped 对象的能力 _service，创建 num_objects 个请求类型的对象。创建 num_objects 个新对象的能力，从 root、node_index 和 node_depth 指定的 CNode 中的 node_offset 开始放置。对于可变大小的内核对象，size_bits 参数用于确定要创建的对象大小。size_bits 与对象大小之间的关系取决于正在创建的对象类型。有关对象大小的更多信息，参见第 2.4.2 节。有关 untyped 内存如何重类型化的更多信息，参见第 2.4 节。有关创建对象能力放置的更多信息，参见第 3.1.3 节。

10.4 x86 特定对象方法

10.4.1 seL4_IRQControl

10.4.1.1 获取 I/O APIC 处理程序

static inline int seL4_IRQControl_GetIOAPIC

为来自 IOAPIC 的中断创建 IRQ 处理程序能力。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.1 节和第 8.2.1 节。

10.4.1.2 获取 MSI 处理程序

static inline int seL4_IRQControl_GetMSI

为来自 MSI 的中断创建 IRQ 处理程序能力。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.1 节和第 8.2.1 节。

10.4.2 seL4_TCB

10.4.2.1 设置 EPT 根

static inline int seL4_TCB_SetEPTRoot

设置线程的 EPT 根

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 6.4 节。

10.4.3 seL4_X86_ASIDControl

10.4.3.1 MakePool

static inline int seL4_X86_ASIDControl_MakePool

创建 X86 ASID 池。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：与作为参数传递的 Untyped Memory 能力一起创建 ASID 池。untyped 能力必须代表 4K 内存对象。这将创建具有 1024 个 VSpace 空间的 ASID 池。

10.4.4 seL4_X86_ASIDPool

10.4.4.1 Assign

static inline int seL4_X86_ASIDPool_Assign

分配 ASID 池。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：将 ASID 分配给作为参数传入的页目录关联的 VSpace。

10.4.5 seL4_X86_EPTPD

10.4.5.1 Map

static inline int seL4_X86_EPTPD_Map

映射 EPT 页目录。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.4.5.2 Unmap

static inline int seL4_X86_EPTPD_Unmap

取消映射 EPT 页目录。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.4.6 seL4_X86_EPTPDPT

10.4.6.1 Map

static inline int seL4_X86_EPTPDPT_Map

映射 EPT 页目录页表。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.4.6.2 Unmap

static inline int seL4_X86_EPTPDPT_Unmap

取消映射 EPT 页目录页表。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.4.7 seL4_X86_EPTPT

10.4.7.1 Map

static inline int seL4_X86_EPTPT_Map

映射 EPT 页表。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.4.7.2 Unmap

static inline int seL4_X86_EPTPT_Unmap

取消映射 EPT 页表。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.4.8 seL4_X86_IOPageTable

10.4.8.1 Map

static inline int seL4_X86_IOPageTable_Map

将 IO 页表映射到 IOSpace 中。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.2.3 节

10.4.8.2 Unmap

static inline int seL4_X86_IOPageTable_Unmap

从 IOSpace 取消映射 IO 页表。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.2.3 节

10.4.9 seL4_X86_IOPort

10.4.9.1 In16

static inline seL4_X86_IOPort_In16_t seL4_X86_IOPort_In16

从 IO 端口读取 16 位。

返回值：如第 8.2.2 节所述的 seL4_X86_IOPort_In16_t 结构。

描述：参见第 8.2.2 节

10.4.9.2 In32

static inline seL4_X86_IOPort_In32_t seL4_X86_IOPort_In32

从 IO 端口读取 32 位。

返回值：如第 8.2.2 节所述的 seL4_X86_IOPort_In32_t 结构。

描述：参见第 8.2.2 节

10.4.9.3 In8

static inline seL4_X86_IOPort_In8_t seL4_X86_IOPort_In8

从 IO 端口读取 8 位。

返回值：如第 8.2.2 节所述的 seL4_X86_IOPort_In8_t 结构。

描述：参见第 8.2.2 节

10.4.9.4 Out16

static inline int seL4_X86_IOPort_Out16

向 IO 端口写入 16 位。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.2.2 节

10.4.9.5 Out32

static inline int seL4_X86_IOPort_Out32

向 IO 端口写入 32 位。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.2.2 节

10.4.9.6 Out8

static inline int seL4_X86_IOPort_Out8

向 IO 端口写入 8 位。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.2.2 节

10.4.10 seL4_X86_IOPortControl

10.4.10.1 Issue

static inline int seL4_X86_IOPortControl_Issue

发布 IO 端口子范围。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.2.2 节

10.4.11 seL4_X86_Page

10.4.11.1 GetAddress

static inline seL4_X86_Page_GetAddress_t seL4_X86_Page_GetAddress

获取底层帧的物理地址。

返回值：seL4_IA32_Page_GetAddress_t 结构，包含 seL4_Word paddr（保存页的物理地址）和 int error。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.4.11.2 MapEPT

static inline int seL4_X86_Page_MapEPT

映射扩展页表。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.4.11.3 MapIO

static inline int seL4_X86_Page_MapIO

将页映射到 IOSpace 中。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.4.11.4 Map

static inline int seL4_X86_Page_Map

将页映射到地址空间或更新映射属性。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：以 VSpace 能力为参数，在给定地址对应的最低级未映射分页结构中安装对给定页的引用，或者如果页已经映射到此地址，则更新映射属性。如果所需的分页结构不存在，此操作将失败，返回 seL4_FailedLookup 错误。

10.4.11.5 Unmap

static inline int seL4_X86_Page_Unmap

取消映射页。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：移除现有映射。

10.4.12 seL4_X86_PageDirectory

10.4.12.1 GetStatusBits

static inline seL4_X86_PageDirectory_GetStatusBits_t seL4_X86_PageDirectory_GetStatusBits

检索映射到地址空间中的页的访问位和脏位。

返回值：seL4_X86_PageDirectory_GetStatusBits_t 结构。

描述：参见第 7 章

10.4.12.2 Map

static inline int seL4_X86_PageDirectory_Map

映射页目录。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.4.12.3 Unmap

static inline int seL4_X86_PageDirectory_Unmap

取消映射页目录。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.4.13 seL4_X86_PageTable

10.4.13.1 Map

static inline int seL4_X86_PageTable_Map

将页表映射到地址空间中。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：以 PageDirectory 能力为参数，在 PageDirectory 中的指定槽安装对被调用 PageTable 的引用。

10.4.13.2 Unmap

static inline int seL4_X86_PageTable_Unmap

从地址空间取消映射页表并将其清零。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：从包含的 PageDirectory 中移除对被调用 PageTable 的引用。参见第 7 章

10.4.14 seL4_X86_VCPU

10.4.14.1 禁用 I/O 端口

static inline int seL4_X86_VCPU_DisableIOPort

在特权执行中禁用 I/O 端口范围

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：在 VCPU 中禁用一定范围的 I/O 端口供执行模式直接访问。

10.4.14.2 启用 I/O 端口

static inline int seL4_X86_VCPU_EnableIOPort

在客户执行中启用 I/O 端口范围

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：在 VCPU 中为执行模式启用一定范围的 I/O 端口供直接访问。请求的端口范围必须是提供的 I/O 端口能力的子范围。这还在提供的 I/O 端口能力和 VCPU 之间建立链接，详情参见第 6.4 节。

10.4.14.3 ReadVMCS

static inline seL4_X86_VCPU_ReadVMCS_t seL4_X86_VCPU_ReadVMCS

从硬件读取 VMCS 字段

返回值：seL4_X86_VCPU_ReadVMCS_t 结构，包含 seL4_Word value（保存 vmread 指令的返回结果）和 int error。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：对 VCPU 对象一部分的 VMCS 区域执行的 vmread 指令的轻量封装。验证请求了合法字段后，vmread 的值直接在结果中返回。

10.4.14.4 SetTCB

static inline int seL4_X86_VCPU_SetTCB

将 TCB 绑定到 VCPU

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：配置 VCPU 和 TCB 的一对一绑定，覆盖两者中的任何先前绑定。参见第 6.4 节。

10.4.14.5 WriteRegisters

static inline int seL4_X86_VCPU_WriteRegisters

将客户模式寄存器设置为给定 seL4_VCPUContext 的字段

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：设置客户模式寄存器，即不属于 VMCS 的任何寄存器。

10.4.14.6 WriteVMCS

static inline seL4_X86_VCPU_WriteVMCS_t seL4_X86_VCPU_WriteVMCS

向硬件写入 VMCS 字段

返回值：seL4_X86_VCPU_WriteVMCS_t 结构，包含 seL4_Word writen（保存用 vmwrite 指令写入的最终值）和 int error。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：对 VCPU 对象一部分的 VMCS 区域执行的 vmwrite 指令的轻量封装。除了验证请求了合法字段外，值可能会被修改以确保硬件中固定的任何位正确，以及内核正确性所需的任何功能不被禁用（参见第 6.4 节）。写入硬件的最终值被返回，可以与输入参数比较以确定内核更改了哪些位。

10.5 IA32 特定对象方法

无方法。

10.6 x86_64 特定对象方法

10.6.1 seL4_X86_PDPT

10.6.1.1 Map

static inline int seL4_X86_PDPT_Map

映射页目录页表。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.6.1.2 Unmap

static inline int seL4_X86_PDPT_Unmap

取消映射页目录页表。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.6.2 seL4_X86_VCPU

10.6.2.1 ReadMSR

static inline seL4_X86_VCPU_ReadMSR_t seL4_X86_VCPU_ReadMSR

从硬件读取 64 位特定 MSR 字段

返回值：seL4_X86_VCPU_ReadMSR_t 结构，包含 seL4_Word value（保存 rdmsr 指令的返回结果）和 int error。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：对特定、需要的寄存器执行的 rdmsr 指令的轻量封装。某些寄存器可能只是被缓存并在稍后恢复。

10.6.2.2 WriteMSR

static inline seL4_X86_VCPU_WriteMSR_t seL4_X86_VCPU_WriteMSR

向硬件写入 64 位特定 MSR 字段

返回值：seL4_X86_VCPU_WriteMSR_t 结构，包含 seL4_Word writen（保存用 wrmsr 指令写入的最终值）和 int error。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：对特定、需要的寄存器执行的 wrmsr 指令的轻量封装。除了验证请求了合法字段外，值可能会被修改以确保硬件中固定的任何位正确，以及内核正确性所需的任何功能不被禁用（参见第 6.4 节）。写入硬件的最终值被返回，可以与输入参数比较以确定内核更改了哪些位。

10.7 ARM 特定对象方法

10.7.1 seL4_ARM_ASIDControl

10.7.1.1 MakePool

static inline int seL4_ARM_ASIDControl_MakePool

创建 ASID 池。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：与作为参数传递的 Untyped Memory 能力一起创建 ASID 池。untyped 能力必须代表 4K 内存对象。这将创建具有 1024 个 VSpace 空间的 ASID 池。

10.7.2 seL4_ARM_ASIDPool

10.7.2.1 ASID 池分配

static inline int seL4_ARM_ASIDPool_Assign

分配 ASID 池。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：将 ASID 分配给作为参数传入的 VSpace。

10.7.3 seL4_ARM_CB

10.7.3.1 AssignVspace

static inline int seL4_ARM_CB_AssignVspace

将 VSpace 分配给上下文库。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.3.1.3 节。

10.7.3.2 CB 清除故障

static inline int seL4_ARM_CB_CBClearFault

清除上下文库的故障状态。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.3.1.7 节。

10.7.3.3 CB 获取故障

static inline seL4_ARM_CB_CBGetFault_t seL4_ARM_CB_CBGetFault

获取上下文库的故障状态。

返回值：seL4_ARM_SMMU_CB_GetFault_t 结构，包含 seL4_Word status（保存上下文库的故障状态）、seL4_Word address（保存故障地址）和 int error。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.3.1.7 节。

10.7.3.4 TLB 无效化

static inline int seL4_ARM_CB_TLBInvalidate

无效化此上下文库中当前 ASID 使用的 TLB 条目。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.3.1.6 节。

10.7.3.5 UnassignVspace

static inline int seL4_ARM_CB_UnassignVspace

取消上下文库的 VSpace 分配。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.3.1.3 节。

10.7.4 seL4_ARM_CBControl

10.7.4.1 GetCB

static inline int seL4_ARM_CBControl_GetCB

创建 CB 能力。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.3.1.2 节。

10.7.4.2 TLB 全部无效化

static inline int seL4_ARM_CBControl_TLBInvalidateAll

无效化所有 TLB 条目。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.3.1.6 节。

10.7.5 seL4_ARM_IOPageTable

10.7.5.1 Map

static inline int seL4_ARM_IOPageTable_Map

将 IO 页表映射到 IOSpace 中。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.2.3 节

10.7.5.2 Unmap

static inline int seL4_ARM_IOPageTable_Unmap

从 IOSpace 取消映射 IO 页表。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.7.6 seL4_ARM_Page

10.7.6.1 清理数据

static inline int seL4_ARM_Page_Clean_Data

将数据缓存清理到 RAM。起始和结束相对于被服务的页。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章。

10.7.6.2 清理并无效化数据

static inline int seL4_ARM_Page_CleanInvalidate_Data

清理并无效化给定页内的缓存范围。该范围将被刷新到 RAM。起始和结束偏移相对于被服务的页。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章。

10.7.6.3 GetAddress

static inline seL4_ARM_Page_GetAddress_t seL4_ARM_Page_GetAddress

获取底层帧的物理地址。

返回值：seL4_ARM_Page_GetAddress_t 结构，包含 seL4_Word paddr（保存页的物理地址）和 int error。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章。

10.7.6.4 无效化数据

static inline int seL4_ARM_Page_Invalidate_Data

无效化给定页内的缓存范围。起始和结束偏移相对于被服务的页，应尽可能对齐到缓存行边界。如果起始和结束未对齐，则对外部缓存行执行额外的清理，以清除请求和缓存行边界之间的字节。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章。

10.7.6.5 MapIO

static inline int seL4_ARM_Page_MapIO

将页映射到 IOSpace 中。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章

10.7.6.6 Map

static inline int seL4_ARM_Page_Map

将页映射到地址空间或更新映射属性。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：以 VSpace 能力为参数，在给定地址对应的最低级未映射分页结构中安装对给定页的引用，或者如果页已经映射到此地址，则更新映射属性。该页不得已经通过此能力映射在不同的 VSpace 或不同的地址；可以通过复制能力将页映射到多个 VSpace 中。

10.7.6.7 统一指令

static inline int seL4_ARM_Page_Unify_Instruction

统一指令缓存。将数据行清理到统一点，无效化相应的指令行到统一点，然后无效化分支预测器。起始和结束偏移相对于被服务的页。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章。

10.7.6.8 Unmap

static inline int seL4_ARM_Page_Unmap

取消映射页。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：移除现有映射。

10.7.7 seL4_ARM_PageTable

10.7.7.1 Map

static inline int seL4_ARM_PageTable_Map

将页表映射到地址空间中。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：以 VSpace 能力为参数，在提供的虚拟地址处将页表的引用安装到 VSpace 中。

10.7.7.2 Unmap

static inline int seL4_ARM_PageTable_Unmap

从页目录取消映射页表并将其清零。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：从包含的页目录中移除对被调用页表的引用。

10.7.8 seL4_ARM_SID

10.7.8.1 绑定 CB

static inline int seL4_ARM_SID_BindCB

将上下文库绑定到流 ID。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.3.1.4 节。

10.7.8.2 解绑 CB

static inline int seL4_ARM_SID_UnbindCB

从流 ID 解绑上下文库。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.3.1.4 节。

10.7.9 seL4_ARM_SIDControl

10.7.9.1 清除故障

static inline int seL4_ARM_SIDControl_ClearFault

清除 SMMU 的故障状态。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.3.1.7 节。

10.7.9.2 获取故障

static inline seL4_ARM_SIDControl_GetFault_t seL4_ARM_SIDControl_GetFault

获取 SMMU 的故障状态。

返回值：seL4_ARM_SMMU_GetFault_t 结构，包含 seL4_Word status（保存 SMMU 的全局故障状态）、seL4_Word syndrome_0（保存 SMMU 的全局故障综合信息 0）、seL4_Word syndrome_1（保存 SMMU 的全局故障综合信息 1）和 int error。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.3.1.7 节。

10.7.9.3 GetSID

static inline int seL4_ARM_SIDControl_GetSID

创建 SID 能力。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.3.1.1 节。

10.7.10 seL4_ARM_VCPU

10.7.10.1 确认虚拟 PPI IRQ

static inline int seL4_ARM_VCPU_AckVPPI

确认先前从 VPPIEvent 故障转发的 PPI IRQ。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：确认并取消屏蔽 PPI 中断，以便后续中断可以通过 VPPIEvent 故障转发。

10.7.10.2 注入 IRQ

static inline int seL4_ARM_VCPU_InjectIRQ

向虚拟 CPU 注入 IRQ。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：用于向 VCPU 排队 IRQ。对于 GICv3 写入 ICH_LRn_EL2，对于 GICv2 写入 LRn，其中 n 由 index 确定。当客户确认注入的中断时，列表寄存器再次可用。

10.7.10.3 读取寄存器

static inline seL4_ARM_VCPU_ReadRegs_t seL4_ARM_VCPU_ReadRegs

读取虚拟 CPU 寄存器。

返回值：seL4_ARM_VCPU_ReadRegs_t 结构，包含 seL4_Word value（保存系统寄存器的值）和 int error（发生错误时为非零）。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：提供读取 EL1 系统寄存器以及 VMPIDR_EL2 的方式。

10.7.10.4 SetTCB

static inline int seL4_ARM_VCPU_SetTCB

将 TCB 绑定到虚拟 CPU。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：虚拟 CPU 和 TCB 之间存在 1:1 关系。如果它们中任一（或两者）与另一个关联，它们将被解除关联，然后与此系统调用中调用的对象关联。

10.7.10.5 写入寄存器

static inline int seL4_ARM_VCPU_WriteRegs

写入虚拟 CPU 寄存器。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：提供写入 EL1 系统寄存器以及 VMPIDR_EL2 的方式。

10.7.11 seL4_IRQControl

10.7.11.1 获取 IRQ 处理程序 (SMP)

static inline int seL4_IRQControl_GetTriggerCore

创建 IRQ 处理程序能力并指定触发方法（边沿或电平）和目标核心。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.1 节。

10.7.11.2 获取带触发类型的 IRQ 处理程序

static inline int seL4_IRQControl_GetTrigger

创建 IRQ 处理程序能力并指定触发方法（边沿或电平）。

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 8.1 节。

10.8 AArch32 特定对象方法

10.8.1 seL4_ARM_PageDirectory

10.8.1.1 清理数据

static inline int seL4_ARM_PageDirectory_Clean_Data

清理页目录内的缓存页

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章。

10.8.1.2 清理并无效化数据

static inline int seL4_ARM_PageDirectory_CleanInvalidate_Data

清理并无效化页目录内的缓存页

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章。

10.8.1.3 无效化数据

static inline int seL4_ARM_PageDirectory_Invalidate_Data

无效化页目录内的缓存页

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章。

10.8.1.4 统一指令

static inline int seL4_ARM_PageDirectory_Unify_Instruction

清理并无效化缓存的指令页到统一点

返回值：返回值 0 表示成功。非零值表示发生错误。参见第 10.1 节了解错误时消息寄存器和标签内容的描述。

描述：参见第 7 章。