1.介绍

SEL4微内核是一个操作系统内核，被设计成在各种应用领域中为系统提供安全、安全和可靠的基础。
作为一个微内核，它为应用程序提供了少量的服务，例如创建和管理虚拟地址空间，线程的抽象，进程间通信的抽象。
内核的小尺寸也有助于对最坏情况下的执行时间进行完整而合理的分析。
本手册从用户的角度描述sel4内核的API。
本文首先简要概述了seL4微内核设计，然后介绍了seL4内核向用户空间公开的高级API。

2.内核服务和对象

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

sel4提供的基本服务如下：

1.线程是支持运行软件的CPU执行的抽象

2.地址空间是每个包含应用程序的虚拟内存空间。应用程序仅限于访问地址空间中的内存

3.进程间通信是经过端点允许线程进行数据传输

4.通知提供了一种类似于二进制信号量的非阻塞信号机制

5.设备原语将设备驱动程序作为非特权应用程序实现。内核通过IPC消息导出硬件设备中断。

6.功能空间存储内核服务的功能(即访问权限)及其簿记信息。（簿记信息是啥？）

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

2.1 基于能力的访问控制

seL4微内核提供了一个基于功能的访问控制模型。

访问控制管理所有内核服务，为了执行操作，应用程序必须调用其拥有的对请求的服务具有足够访问权限的功能。

这样，系统就可以被配置为相互隔离软件组件，并且通过有选择地授予特定的通信能力，在组件之间启用授权的、受控的通信。
这使得软件组件隔离具有高度的保证，因为只有那些由能力占有明确授权的操作才被允许。

一个功能是一个不可伪造的令牌，它引用一个特定的内核对象（比如线程控制块），并携带控制哪些方法可能被调用的访问权限。

从概念上讲，能力存在于应用程序的能力空间中；这个空间中的地址指的是一个插槽，它可能包含也可能不包含能力。

应用程序可以引用一个内核服务的能力，例如使用拥有该能力的插槽的地址。
这意味着，seL4能力模型是隔离(或分区)能力系统的实例，其中的能力由内核管理。

能力空间被实现为一个由内核管理的能力节点(cnode)组成的有向图。CNode是一个槽位表，每个槽位可能包含更多的CNode功能。
能力空间中的能力地址是插槽索引与节点索引的串联，形成到目标插槽的路径（这一点后续再看）

功能可以在功能空间内复制和移动，也可以通过ipc传送。这个允许创建具有特定访问权限的应用程序，将权限委派给另一个应用程序，并将应用程序权限传递给新创建（或选定）的内核服务。此外，还可以使用原始功能的一部分权限创建派生功能（决不能使用更多权限）。新创建的功能可用于部分授权。

还可以撤销功能从而撤销权限，撤销将递归地删除从被撤销的原始功能派生出来的任何功能。功能在系统中的传播由一个基于许可的模型控制。

2.2 系统调用

seL4内核提供了一个消息传递服务，用于在线程。这个机制还用于与内核提供的服务进行通信。有一个标准的消息格式，每个消息包含一些数据字和一些可能的功能。第四章详细描述了这些消息的结构和编码。

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

逻辑上，内核提供三个系统调用:发送、接收和输出。然而，也有一些基本的Send和Receive调用的组合和变体，例如Call操作，它由来自同一个对象的一个Send和一个Receive组成。

除了端点和通知之外，内核对象上的方法都映射到发送或调用，这取决于方法是否返回结果。（端点，通知还有方法是什么？）
Yield系统调用不与任何内核对象相关联，并且是唯一不调用功能的操作。

完整的系统调用：
sel4_send：通过指定的功能和应用程序传递消息以继续。如果调用的功能是一个端点，并且没有接收者准备好立即接收消息，则发送线程将阻塞，直到消息可以被传递。
sel4_NBSend：在端点上执行轮询发送。它与sel4send（）类似，只是保证不会阻塞。如果消息不能立即传递，即没有接收者在目标点等待，则消息会自动丢弃。
sel4_recv：由线程用于通过端点或通知接收消息。如果没有发件人或通知处于挂起状态，则调用者将阻塞，直到可以传递消息或通知为止。此系统调用仅适用于一个点或非通知功能，在尝试使用其他功能类型时会引发错误。
sel4_Call：该调用将阻塞发送方线程，直到其消息被传递并收到回复消息为止，当sent消息被传递到另一个线程（通过endpoint）时，内核向传递到接收方的消息添加了一个额外的“reply”功能，使接收方有权回复原始发送方。应答能力存放在接收方的TCB中的一个专用插槽中，是一个单一的使用权，这意味着内核一旦被调用就会使它失效。
sel_Reply：用于应答sel_call的，并使用产生于sel_call系统调用的应答功能，并存储在回复线程的TCB中。
sel_ReplyRecv：是sel_reply和sel_recv的结合，它存在的主要原因是：通常情况下，响应一个请求并等待下一个请求可以在单个内核系统调用中执行，而不是在两个内核系统调用中执行。从应答到接收阶段的转换也是原子的。
sel_NBRecv:线程使用它来检查通知对象上挂起的信号或端点上挂起的消息，而不阻塞。此系统调用仅适用于端点和通知对象功能.
sel4_Yield:是唯一不需要使用某种功能的系统调用。它会丧失调用线程的时间片的剩余部分，并导致调用内核的调度程序。如果没有其他与调用者具有相同优先级的可运行线程，调用线程将立即使用新的时间片调度。

2.3 内核对象

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

CNodes：存储功能，允许线程调用特定对象上的方法，每个节点都有固定数量的插槽（slot），通常是2的幂，这取决于节点的创建时间，插槽可以是空的也可以包含功能。

线程控制块（TCB）：表示seL4中的一个运行线程，线程是调度、阻塞、非阻塞等的执行单元，具体取决于应用程序与其他线程的交互。

Endpoints：促进了进程之间的消息传输，IPC是同步的：试图在端点上发送或接收消息的线程会阻塞，直到消息可以传递为止，这意味着只有当发送者和接受者在端点汇合时，消息传递才会发生，内核可以通过一个拷贝传递消息。
端点的功能可以被限制为只发送或只接收。此外，端点功能可以拥有授予权，这允许将功能作为消息的一部分发送

通知对象：提供一个简单的信号机制。一个通知是一个字大小的标志数组，每个标志的行为都像一个二进制信号量。操作在单个操作中向标志的子集发出信号，轮询检查任何标志，并阻塞直到任何标志被发出信号。通知功能可以是仅限信号的或仅限等待的。

虚拟地址空间对象：用于为一个或多个线程构造虚拟地址空间，这些对象很大程度上直接对应于硬件对象，因此依赖于体系结构。内核还包括用于跟踪地址空间状态的ASID池和ASID控制对象。

中断对象：中断对象给应用程序接收和确认来自硬件设备的中断的能力。最初，IRQControl有一个功能，它允许创建IRQHandler功能。IRQHandler能力允许管理与特定设备相关联的特定中断源。它被委托给一个设备驱动程序来访问中断源。IRQHandler对象允许线程等待并确认单个中断。

非类型化内存：无类型内存是sel4内核中内存分配的基础。非类型化内存功能只有一个方法，允许创建新的内核对象。如果方法成功，调用线程将获得对新创建对象的功能的访问权。此外，非类型化内存对象可以划分为一组较小的非类型化内存对象，允许委托部分(或全部)系统内存。我们在下面的章节中一般地讨论内存管理。

2.4 内核内存分配

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

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

使用seL4 Untyped Retype()创建对象的用户级应用程序，将接收对结果对象的全部权限。然后，它可以将其对该对象拥有的全部或部分权限委托给一个或多个客户端。

非类型化内存对象表示两种不同类型的内存：通用内存或设备内存
通用内存可以非类型化为任何其他对象类型，并用于内核提供的非类型化内存上的任何操作。设备内存覆盖由硬件平台决定的为设备预留的内存区域，这些对象的使用受到内核的以下方式的限制:

设备非类型化对象只能重新键入到帧或其他非类型化对象中；例如，开发人员不能从设备内存创建端点
从设备中重新类型化的帧对象不能设置为线程IPC缓冲区，或用于创建ASID池

子无类型对象的类型属性（是否表示的是通用或设备内存）继承父亲的无类型对象，也就是说，未类型化设备的任何子设备也将是一个未类型化设备。开发人员不能更改无类型的类型属性。

2.4.1 重用内存

到目前为止所描述的模型对于应用程序分配内核对象、在客户机应用程序之间分配权限以及获得这些对象提供的各种内核服务是足够的。对于一个简单的静态系统配置来说，这一点就足够了。

seL4内核还允许重用非类型化内存区域。只有当内存中的对象没有悬空引用（即功能）时，才允许重用内存区域。（悬空引用是啥）
这样生成的树结构称为能力派生树（CDT）。2例如，当用户通过重新键入非类型化内存来创建新的内核对象时，新创建的功能将作为非类型化内存功能的子功能插入CDT。

对于每个非类型化内存区域，内核保留一个水印，记录之前分配了多少区域。每当用户请求内核在非类型化内存区域中创建新对象时，内核将执行以下两种操作之一:
如果区域中已经分配了现有对象，内核将在当前水印级别分配新对象，并增加水印。如果所有先前在区域中分配的对象都已被删除，内核将重置水印并从区域开始重新分配新对象。

最后，CNode对象提供的seL4 CNode Revoke()方法销毁了从参数capability派生的所有功能。将最后一个功能撤消到内核对象会触发对现在未引用的对象的销毁操作。这只是清除它、其他对象和内核之间的任何内核依赖关系。

通过对非类型化内存对象的原始功能调用sel4cnoderevoke（），用户将删除非类型化内存对象的所有子对象，即指向非类型化内存区域中对象的所有功能。因此，在这个调用之后，没有对非类型化区域中的任何对象的有效引用，可以安全地重新键入和重用该区域。

2.4.2 对象大小总结

在重新键入非类型化内存时，了解对象需要多少内存是很有用的。表2.1、2.2和2.3总结了物体尺寸。

注意cnode和非类型化对象有变量大小。当将非类型化内存重新键入cnode或将非类型化对象分解为更小的非类型化对象时，使用seL4 untyped Retype()的size bits参数来指定结果对象的大小。表2.1显示了size bits参数(n)与seL4 Untyped Retype()之间的对应关系，以及每个可变大小对象的结果大小。

对于所有其他对象类型，大小是固定的，seL4-Untyped_Retype()的size_bits_参数被忽略。对seL4UntypedRetype()的一次调用可以将单个无类型对象重新键入为多个对象。要创建的对象数量由它的num_objects参数指定。所有创建的对象必须具有相同的类型，由type参数指定。对于可变大小的对象，每个对象也必须具有相同的大小。如果所需内存区域的大小(通过对象大小乘以num_objects来计算)大于未类型化对象剩余的未分配内存，则会产生错误。

3.功能空间

回想一下第2.1节，seL4实现了基于功能的访问控制模型。每个用户空间线程都有一个关联的功能空间(CSpace)，它包含线程所拥有的功能，从而控制线程可以访问哪些资源。

回想一下，功能驻留在称为cnode的内核管理对象中。CNode是一个槽位表，每个槽位可能包含一个功能。这可能包括进一步扩展cnode的功能，形成一个有向图。从概念上讲，线程的CSpace是有向图中从CNode能力(CSpace根)开始就可到达的部分。

CSpace地址指的是一个单独的插槽(在CSpace中的某些cnode中)，它可能包含也可能不包含功能。线程在它们的cspace中使用存放该功能的槽的地址来引用功能。在CSpace中的一个地址是CNode能力的索引的连接，形成到目标槽的路径;

功能可以在CSpace中复制和移动，也可以在消息中发送，此外，新的功能可以从旧的功能中的权限子集来获得。seL4维护了功能派生树(CDT)，它在其中跟踪这些复制的功能与原始功能之间的关系。revoke方法删除了从所选功能派生的所有功能(在所有cspace中)。服务器可以使用这种机制来恢复它们提供给客户端的对象的唯一权限，或者非类型化内存的管理器可以使用这种机制来销毁内存中的对象，以便重新类型化。

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

3.1 能力和能力空间的管理

3.1.1 CSpace的创建

CSspace是通过创建和操作CNode对象而创建的。创建一个CNode时，用户必须指定它将拥有的插槽数，这决定了它将使用的内存量。每个插槽需要16个字节的物理内存，并且有恰好容纳一种能力的容量。
像任何其他对象一样，CNode必须通过在适当数量的非类型化内存上调用seL4UntypedRetype()来创建(参见2.4.2节)。因此，调用者必须能够在现有cnode中获得足够的非类型化内存以及足够的空闲能力槽，以便seL4UntypedRetype()调用成功。

3.1.2 CNode方法

功能主要通过调用CNode方法来管理。
CNode支持以下方法：
sel4_cnode_mint（）：从现有功能在指定的CNode插槽中创建新功能。新创建的功能可能比原功能拥有更少的权限，并且有一个不同的保护。sel4nodemint()也可以从一个未标记的功能创建一个标记的功能。

sel4_cnode_copy()：与sel4_cnode_mint（）类似，但新创建的功能与原来的功能具有相同的标记和保护。

sel4_cnode_move（）：在两个指定的功能插槽之间移动功能。不能将功能移动到当前所在的插槽中。

sel4_cnode_mutate():可以类似于sel4_cnode_move（）移动功能，也可以类似于sel4_cnode_mint（）减少其权限，但不保留原始副本。

sel4_cnode_rotate():在三个指定的能力槽之间移动两个能力。它实际上是两个seL4CNodeMove()调用:一个从指定的第二个插槽到第一个插槽，一个从指定的第三个插槽到第二个插槽。第一个和第三个指定的槽位可能相同。

sel4_cnode_delete():删除指定slot的能力。

sel4_cnode_revoke():相当于对指定功能的每个派生子级调用sel4_cnode_delete（）。它对能力本身没有影响，除非在第3.2节中概述的非常特殊的情况下。

sel4_cnode_savecaller():将当前线程的内核生成的应答能力从创建它的特殊TCB插槽移动到指定的CSpace插槽。

sel4_cnode_cancelbadgesends():取消任何使用相同标记和对象作为指定功能的未完成发送。

3.1.3 新重新类型化对象的功能

当使用seL4UntypedRetype()将未类型化内存重新类型为对象时，新重新类型化对象的功能将被放置在CNode的连续槽中，该CNode由根、node_index和node_depth参数指定。node_offset参数指定将放置第一个能力的CNode的索引。num_objects参数指定要创建的功能(以及对象)的数量。所有插槽必须为空，否则将导致错误。所有产生的功能都将放在同一个CNode中.

3.1.4 能力权利

如前所述，某些功能类型具有与之相关联的访问权限。目前，访问权限与端点(见第4章)、通知(见第5章)和页面(见第7章)的功能相关联。与功能相关联的访问权限决定了可以调用的方法。seL4支持三种正交访问权限，即读、写和授予。每个权利的含义是相对于各种对象类型进行解释的，详见表3.1。
第一次创建对象时，引用它的初始能力携带最大访问权限集。使用诸如sel4nodemint()和sel4 cnodemutate()之类的方法，可以从这个原始功能中制造出其他不那么强大的功能。如果在这些调用中的任何一个中，为目标功能指定了比源功能更大的权限集，那么目标权限将被静默地降级为源权限。

3.1.5 能力派生树

正如2.4.1节中提到的，seL4在一个能力派生树中跟踪能力派生。
各种方法，如seL4CNodeCopy()或sel4 cnode mint()，可以用于创建派生功能。并不是所有的功能都支持派生。通常，只有原始功能支持派生调用，但也有例外。
总结各种能力类型的能力派生要成功必须满足的条件，以及如何在每个案例中报告能力派生失败。未列出的功能类型只能派生一次。

显示了一个示例功能派生树，该树演示了一个标准方案，顶层是一个大型非类型化功能，第二层将此功能拆分为两个区域，由他们自己的非类型化功能覆盖，这两层都是第一层的子集，左侧的第三级是第二级非类型化功能的副本，复制时的非类型能力总是创建子级，而不是兄弟级，在这个场景中，非类型化功能被输入到两个独立的对象中，在级别4上创建两个功能，它们都是各自对象的原始功能，都是从中创建的非类型化功能的子功能。
普通的原始功能可以有一个级别的派生功能。这些派生功能的进一步复制将创建兄弟版本，在这种情况下仍在级别5上。对于端点和通知功能，这个方案有一个例外——它们通过标记支持额外的一层深度。原始端点或通知功能将被取消标记。使用mint方法，可以创建具有特定徽章的功能副本(见第4.2.1节，第5.1节)
同一个对象的这个新的、带标记的功能被视为原始功能(“原始带标记端点功能”)，并像其他功能一样支持一个派生的子级别

3.2 删除和撤销

seL4中的功能可以被删除和撤销。这两种方法都主要影响能力，但它们可能对系统中的对象产生副作用，因为删除或调用会导致对对象的最后一种能力的破坏。

如上所述，seL4CNodeDelete（）将从指定的节点插槽中删除功能。通常，这就是所有发生的事情。但是，如果它是某个对象的最后一个类型功能，那么这个对象现在将被内核销毁，清除内核引用中剩余的所有内容，并准备内存以供重用。

如果要销毁的对象是一个能力容器，即TCB或CNode，销毁过程将在销毁容器之前删除容器中保存的每个能力。如果包含的功能是最后的功能，这可能导致进一步对象的销毁。

sel_cnode_revoke方法将删除派生树中指定功能的所有子功能，但是功能的本身不变，如果任何已撤销的子功能是对象的最后一个功能，则会触发相应的销毁操作。

注意:sel4cnoderrecall()可能在两种特定情况下只能部分完成。第一个是包含执行撤销的线程的TCB的最后一个功能(或TCB本身的最后一个功能)的CNode由于撤销而被删除。在这种情况下，执行撤销的线程在触发期间被销毁，撤销未完成。

第二种情况是，包含作为吊销目标的功能的存储作为吊销的结果被删除。在这种情况下，执行吊销的权限将在操作过程中被删除，并且操作会中途停止。这两种情况都可以而且应该通过构造在用户级别避免。
注意，对于页表和页目录，sel4cnoderrecall()不会撤销映射到地址空间的帧功能。他们只会在空间中消失。

3.3 CSpace 寻址

在执行系统调用时，线程通过在其CSpace中提供地址来向内核指定要调用的功能。此地址是指调用方的CSpace中包含要调用的功能的特定插槽。
cspace的设计允许稀疏性，并且查找功能地址的过程必须是高效的。因此，cspace被实现为受保护的页表。

如前所述，CSpace是CNode对象的有向图，每个CNode是一个槽位表，其中每个槽位可以是空的，也可以包含一个功能，该功能可以引用另一个CNode。回想一下2.3节，CNode中的插槽数必须是2的幂。CNode有一个基数，也就是2的幂的大小，也就是说，如果一个CNode有2k个槽位，那么它的基数就是k。内核在线程的TCB中存储每个线程CSpace的根CNode的能力。从概念上讲，CNode功能不仅存储对它所引用的CNode的引用，而且还携带一个保护值，见3.3.1节。

3.3.1 功能地址查找

与虚拟内存地址一样，功能地址只是一个整数。与引用物理内存的位置(如虚拟内存地址)不同，能力地址引用能力槽。当查找用户空间线程提供的功能地址时，内核首先查询线程的TCB中的CNode功能，该TCB定义了线程的CSpace的根。
然后，它将CNode的保护值与能力地址的最有效位进行比较。如果这两个值不同，则查找失败。如果保护位是相同的，要看这个radix位，它最终可能指向下一个cnode，这个cnode包含我们要找的能力。那个slot可能包含cnode也可能包含其他东西，也可能啥都没有。
如果s包含一个CNode能力c，并且能力地址中还有剩余的位(在radix之后)还没有被转换，那么就会重复查找过程，从CNode能力c开始，并使用能力地址的剩余位。否则，查找过程成功终止;此处的能力地址指的是能力槽。

顶级CNode对象，12位保护设置为0x000和256个插槽
具有直接对象引用的顶级CNode
具有两个二级CNode引用的顶级CNode
具有不同防护和槽数的二级CNodes
第二级CNode，包含对顶级CNode的引用
第二级CNode，包含对另一CNode的引用，其中还有一些位需要翻译
第二级CNode，其中包含对另一CNode的引用，其中没有剩余的位要被翻译
第二级CNodes中的对象引用

3.3.2 寻址能力

能力地址存储在一个CPointer(缩写为CPTR)中，它是一个无符号整数变量。根据上面描述的翻译算法处理功能。两种特殊情况涉及到CNode能力本身的寻址和一系列能力槽的寻址。

回想一下，上面描述的转换算法将遍历CNode功能，但仍有需要转换的地址位。因此，为了为CNode能力寻址，用户不仅必须提供一个能力地址，而且必须指定要转换的能力地址的最大位数，称为深度限制。

某些方法，如seL4UntypedRetype()，要求用户提供一系列的功能槽。这是通过提供一个base capability address(引用范围中的第一个槽位)和一个window size参数来实现的，该参数指定范围内槽位的数量(在基槽位之后有连续的地址)。

Cap A：第一个CNode有一个设置为0x0的4位保护和一个8位基数。Cap位于插槽0x60中，因此它可以被格式为0x060xxxxx的任何地址引用（其中xxxxx是任意数字，因为翻译过程在翻译地址的前12位之后终止）。为简单起见，我们通常采用地址0x06000000

Cap B：同样，第一个CNode有一个4位保护设置为0x0，还有一个8位基数。第二个CNode通过L2 CNode cap到达。它还有一个4位保护0x0，Cap B驻留在索引0x60处。因此，Cap B的地址是0x00F06000。此地址的转换在前24位之后终止。

Cap C：这种能力是通过两个CNodes来实现的。第三个CNode通过L3 CNode Cap到达，该Cap位于第二个CNode的索引0x00处。第三个CNode没有防护罩，而Cap C位于索引0x60处。因此，它的地址是0x00f00060。此地址的翻译将保留0位未翻译

Cap C-G：通过提供0x00F00060的基址（指包含Cap C的插槽）和5的窗口大小来寻址这个能力插槽范围。

L2 CNode Cap：回想一下，要定位CNode功能，用户不仅必须提供功能地址，还必须指定深度限制，即要转换的最大比特数。L2 CNode Cap位于firstCNode的偏移量0x0F，该节点有一个4位的0x0保护。因此，它的地址是0x00F00000，深度限制为12位。

L3 CNode Cap：这个功能位于第二个CNode的索引0x00，由L2 CNode Cap到达。第二个CNode有一个4位的0x0保护。因此，该功能的地址为0x00F00000，深度限制为24位。注意L2和L3 CNode Caps的地址是相同的，但是它们的深度限制是不同的。

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

3.4 查找失败描述

当功能查找失败时，将向调用线程或线程的IPC缓冲区中的异常处理程序提供失败的描述。描述的格式总是相同的，但根据错误发生的方式，IPC缓冲区中的偏移量可能不同。描述格式如下所示。第一个单词表示查找失败的类型，后面单词的含义取决于此。

3.4.1 无效的根

CSpace CPTR根目录（在其中查找功能）无效。例如，该功能不是aCNodecap

3.4.2 缺失能力

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

3.4.3 深度不匹配

在解析一个功能时，遍历一个CNode，该CNode解析的比特数超过了CPTR中留给解码的比特数，或者遇到了一个非CNode功能，但仍有剩余的比特需要查找

3.4.4 保护不匹配

解析功能时，CNode的保护大小大于剩余的位数，或者CNode的保护与解析的PTR的下一位不匹配

4.IPC

seL4微内核为线程间的通信提供了一种消息传递IPC机制。同样的机制也用于与内核提供的服务进行通信。通过调用内核对象的功能来发送消息。发送到端点的消息被指定给其他线程，而发送到其他对象的消息则由内核处理。本章描述通用的消息格式、端点，以及如何将它们用于应用程序之间的通信。

4.1 消息寄存器

每个消息都包含一些消息字和可选的一些功能。消息字通过将它们放置在线程的消息寄存器来发送或接收。消息寄存器被编号，前几个消息寄存器是使用物理CPU寄存器实现的，而其余的由一个称为IPC缓冲区的固定内存区域支持。

这种设计的原因是效率：非常短的消息不需要使用内存，物理CPU消息寄存器如下所示

每个IPC消息也有一个标记(结构为seL4MessageInfo_t)。标签由四个字段组成:标签、消息长度、功能数量(extraCaps字段)和capsUnwrapped字段。消息长度和功能的数量决定了发送线程希望传输的消息寄存器和功能的数量，或者决定了实际传输的消息寄存器和功能的数量。标签不被内核解释，它作为消息的第一个数据有效负载未经修改地传递。例如，标签可以用来指定请求的操作。
capsUnwrapped字段仅在接收端使用，用于指示接收功能的方式。第4.2.2节对此进行了描述。

内核假设IPC缓冲区包含表4.3中定义的seL4IPCBuffer类型的结构。内核使用尽可能多的物理寄存器来传输IPC消息。当传输的参数多于可用的物理消息寄存器时，内核开始使用IPC缓冲区的msg字段来传输参数。但是，它在这个数组中为物理消息寄存器留下了空间。

例如，如果IPC传输或内核对象调用需要4个消息寄存器(在这个体系结构上只有2个物理消息寄存器可用)，那么参数1和2将通过消息寄存器传输，参数3和4将在msg[2]和msg[3]中。
如果需要，这允许用户级对象调用存根将在物理寄存器中传递的参数复制到msg数组的剩余空间。tag字段的情况类似。在seL4IPCBuffer结构中有这个字段的空间，内核会忽略它。用户级存根可能希望将消息标签从其cpu寄存器复制到此字段，尽管内核提供的用户级存根不这样做。

4.2 Endpoints

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

IPC端点使用集合模型，因此是同步和阻塞的。端点对象可以对发送或接收的线程进行排队。如果没有接收方准备好，执行seL4Send()或seL4Call()系统调用的线程将在队列中等待第一个可用的接收方。同样，如果没有准备好发送方，执行seL4Recv()系统调用或seL4ReplyRecv()的后半部分的线程将等待第一个可用的发送方。

4.2.1 endpoint badges

可以创建端点功能，以创建带有badge(由mint操作的调用者选择数据字)的新端点功能。当用baged权能发送消息到端点时，badge被转移到接收线程的badge寄存器。

带有零标记的端点功能被称为unbadge。这样的功能可以在包含该功能的CNode上使用seL4CNodeMutate()或sel4cnnodemint()调用进行标记。带有徽章的端点功能不能被取消标记、重新标记或用于创建带有不同徽章的子功能。

只有低28位的徽章可以使用。内核会无声地忽略任何高4位的使用

4.2.2 权能转移

如果发送线程调用的端点功能具有授予权限，则消息可能包含将被传输到接收方的功能。尝试在没有授权的情况下使用端点功能发送功能，将导致原始消息的传输，而没有任何功能的传输。

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

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

接收端能力与原始能力拥有相同的权利，除非接收端能力缺乏写权限。在这种情况下，通过从接收的功能副本中剥离写权限，对发送功能的权限被削弱。

请注意，接收线程可以只指定一个接收槽，而发送线程可以在消息中包含多个功能。包含多个功能的消息可以由内核对象解释。在消息中的一些额外功能可以展开的情况下，还可以将它们发送给接收线程。

如果第n个能力指的是端点的消息通过消息发送,能力是打开:它的徽章是放在第n个位置数组接收机的徽章,和内核设置第n个点(从最低有效计数)capsUnwrapped消息的字段标签。能力本身没有被转移，所以接收槽可以被用于另一个能力。

如果接收方收到一条消息，其标签的extraCaps为2,capsUnwrapped为2，则消息中的第一个能力被转移到指定的接收槽，第二个能力被打开，将其徽章放置在徽章中。发送者的邮件中可能存在无法打开的第三种功能。

sel4 手册总结之介绍与内核服务和对象相关推荐

交互式电子手册软件系统(IETM)介绍
交互式电子手册软件系统(IETM)介绍华盛恒辉交互式电子手册(IETM-Interactive Electronic Technical Manual)是针对配备.设备或大型工程零碎设计的技术手册数 ...
char怎么比较_为什么阿里巴巴Java开发手册中强制要求整型包装类对象值用 equals 方法比较？...
在阅读<阿里巴巴Java开发手册>时,发现有一条关于整型包装类对象之间值比较的规约,具体内容如下: 这条建议非常值得大家关注, 而且该问题在 Java 面试中十分常见. 还需要思考以下几个 ...
领英精灵使用手册，功能介绍
领英精灵手册下载及安装一键批量加好友批量撤回邀请好友分组.备注管理深度挖掘客户资料一键导出客户资料一键批量群发消息禁发名单一键批量点赞参数设置会员权限常见问题下载及安装下载 ...
Vue3手册译稿 - 基础 - 介绍
介绍提示已经了解Vue2且仅想知道Vue3有哪些新功能?请参阅迁移指南 Vue.js是什么? Vue(读音/vjuː/,像view一样发音)是一套用于构建用户界面的先进框架,不像其他僵化的框架,V ...
Python学习手册之Python介绍、基本语法（二）
在上一篇文章中,我们介绍了Python的一些基本语法,现在我们继续介绍剩下的Python基本语法.查看上一篇文章请点击:https://www.cnblogs.com/dustman/p/987193 ...
1504_AURIX_TC275参考手册_芯片介绍
全部学习汇总: GreyZhang/g_TC275: happy hacking for TC275! (github.com) 逐渐开始了解MCU的功能了,我发现RM手册躲不过去了.与其见招拆招,倒 ...
三星emmc芯片手册_eMMC详细介绍
质量记录编号姓名工号学历本科专业计算机科学与技术部门岗位入职时间深度了解 eMMC 一． eMMC 的概述 eMMC (Embedded MultiMedia Card) 为 ...
简单介绍实体类或对象序列化时,忽略为空属性的操作
这篇文章主要介绍了实体类或对象序列化时,忽略为空属性的操作,具有很好的参考价值,希望对大家有所帮助.如有错误或未考虑完全的地方,望不吝赐教第一种,在配置文件配置在application.xml直接 ...
window点location（仅介绍window点location对象，不介绍属性，因标题不能含有非法字符，.用点来代替）
文章目录 1.前言: 2.window.location介绍 3.做CTF题时遇到的代码 4.总结 1.前言: 这个是我做CG-CTF-Web-单身二十年时遇到的,这里就该题简单总结一下 2.wind ...
python类和对象介绍_Python开发基础-Day17面向对象编程介绍、类和对象
面向对象变成介绍面向过程编程核心是过程(流水线式思维),过程即解决问题的步骤,面向过程的设计就好比精心设计好一条流水线,考虑周全什么时候处理什么东西.主要应用在一旦完成很少修改的地方,如linux ...

sel4 手册总结之介绍与内核服务和对象