官网链接：link

求解

代码中的很多方法例如这一个教程里面的seL4_GetMR(0)，我在官方给的手册和API中都搜不到，想问一下大家这些大家都是在哪里搜的！！

IPC

seL4中的IPC和一般OS中讲的IPC概念相差比较大，根据官方的意思是理解seL4的IPC的时候，最好忘记IPC的概念，起这个名字只是为了标准上对齐，但是理解的时候最好将其当作专有名词来理解。

背景知识

进程间通信（IPC）是用于在进程之间同步传输少量数据和能力的微内核机制。在seL4中，称为端点的小型内核对象促成了IPC，端点充当的是通讯的端口。端点对象的调用通常被用于收发IPC数据。
端点们由一系列的等待收发信息的线程组成。为了理解这一点，思考一个案例：n个线程正在一个端点上等待一个信息。如果n个端点在一个端点上发送信息，那么n个在该端点上等待信息的线程都将会收到这些信息且被唤醒。如果此时有第n+1个发送者发送一个信息，那么这个发送者将会排队等待。

系统调用

线程可以通过系统调用seL4_Send在端点上发送信息，一直阻塞到信息被其他线程接收的时候。seL4_NBSend也可以用，它执行轮询发送：该发送仅当已经有一个线程阻塞等待一个信息的时候才会发送成功，否则就失败。为了避免出现反向通道，seL4_NBSend不返回指示消息是否已发送的结果。
seL4_Recv 可用于接收消息，seL4_NBRecv 可用于轮询消息。
seL4_Call是一个系统调用，本质上结合了seL4_Send和seL4_Recv，但是有一个主要区别：在接收阶段，使用此函数的线程被阻塞在一个一次性能力上，称为回复能力（reply capability），而不是在端点本身上。在client-server场景下，客户端使用seL4_Call发出请求，服务器可以显式的回复正确的客户端。
回复能力（reply capability）内部存储在接收者的线程控制块（TCB）中。系统调用 seL4_Reply 会调用这个能力，向客户端发送一个进程间通信（IPC）并将其唤醒。seL4_ReplyRecv 也执行相同操作，但它在一个组合的系统调用中发送回复并阻塞在提供的端点上。
由于线程控制块（TCB）只有一个空间来存储回复能力（reply capability），如果服务器需要处理多个请求（例如在硬件操作完成后再进行回复），可以使用 seL4_CNode_SaveCaller 将回复能力保存到接收者的 CSpace 中的一个空槽中。

方法	说明
seL4_Send	发送后阻塞，直到对方接收之后才会取消阻塞
seL4_NBSend	非阻塞发送，发送后继续往下执行，但不告知发送结果，防止反向通道
seL4_Call	立即发送，阻塞等待回复，该回复不是说对方发消息的回复，而是使用seL4_Reply进行回复，才会取消阻塞继续往下执行
seL4_Reply	响应的功能，只有他能唤醒call调用的阻塞，也可唤醒seL4_Recv的阻塞
seL4_Recv	阻塞等待，直到有消息到达，这个消息可以是回复（Send、NBSend），也可以是响应Reply

反向通道 （back channel）

back channel（反向通道） 指的是一种非预期的或隐藏的信息传递路径，可能会导致信息泄露或安全问题。通常，在操作系统或安全系统中，设计者希望确保通信通道只能按照预期的方式工作，防止信息通过其他途径（即“反向通道”）泄露。在 seL4_NBSend 的情况下，如果系统返回了消息是否成功发送的结果，发送者就能通过这个结果推断接收者的状态（例如，接收者是否正在等待消息）。这就可能成为一个反向通道，允许一个线程获取另一个线程的状态信息，而这类信息可能会被滥用。因此，seL4_NBSend 不返回结果来避免这种潜在的安全隐患。

IPC Buffer

每个线程都有一个Buffer（被称之为IPC Buffer），它包含IPC消息，是由数据和能力组成的。发送发指定消息长度，内核在发送方和接收放IPC缓冲区之间复制此（有界）长度。

Data transfer

IPC 缓冲区包含用于在 IPC 上传输数据的消息寄存器 (MR) 有界区域。每个寄存器都是机器字大小，最大消息大小可在 libsel4 提供的 seL4_MsgMaxLength 常量中找到。
可以使用seL4_SetMR 将消息加载到IPC 缓冲区中，并使用seL4_GetMR 提取消息。小消息在寄存器中发送，不需要复制操作。适合寄存器的字数可在 seL4_FastMessageRegisters 常量中获得。
所传输的数据量（根据所使用的消息寄存器的数量）必须设置为 seL4_MessageInfo_t 数据结构中的长度字段。

消息寄存器和IPC缓冲区之间的关系

1、消息寄存器

• 消息寄存器是 seL4 内核用于短消息传递的一个内部概念。在 seL4 中，系统为每个线程分配了一些虚拟寄存器，用于存储发送和接收的消息数据。这些消息寄存器主要用于传递少量数据（例如几字节到几百字节）。在处理简单的 IPC 传递时，寄存器用来保存消息内容。
• seL4_GetMR(index) 函数的作用就是访问某个消息寄存器中的数据。index 代表消息寄存器的索引号，比如 0 代表第一个消息寄存器。

2、IPC buffer

• IPC buffer 是 seL4 中的一个内存区域，用于消息传递。当消息过大、超出了消息寄存器的容量时，IPC buffer 才被使用。IPC buffer 位于线程控制块 (TCB) 中，线程可以通过这个缓冲区来传递大消息或能力等复杂的数据结构。
• 也就是说，小消息存储在消息寄存器中，而大消息存储在 IPC buffer 中。

3、二者之间的关系

• 当 seL4 处理 IPC 消息时，它首先会使用消息寄存器来传递较小的消息（这比访问内存中的 IPC buffer 更快）。
• 如果消息的大小超过了消息寄存器的容量，系统会将它分片后存入 IPC buffer，寄存器中只保存与此消息相关的元数据或控制信息。

Cap transfer

除了数据之外，IPC 还可用于在每个消息的进程之间发送能力。这称为能力转移。正在传输的能力数量在 seL4_MessageInfo_t 结构中编码为 extraCaps。下面是通过 IPC 发送能力的示例：

seL4_MessageInfo info = seL4_MessageInfo_new(0, 0, 1, 0);
seL4_SetCap(0, free_slot);
seL4_Call(endpoint, info);

以前是玩过单片机，看到这个寄存器的时候十分敏感，总觉得是硬件寄存器。此处的寄存器指的是IPC消息的能力槽位(capability slot)中。所以上面的seL4_SetCap(0, free_slot) 的作用是把free_slot这个能力放到IPC消息info的第一个能力槽位中（槽位索引为0）。
若想要接收能力，接收者必须指定一个 cspace 地址来放置该能力。这如下面的代码示例所示：

seL4_SetCapReceivePath(cnode, badged_endpoint, seL4_WordBits);
seL4_Recv(endpoint, &sender);

接收到的能力的访问权限与接收者对端点拥有的权限相同。请注意，虽然发送方可以发送多种功能，但接收方一次只能接收一种功能。

Capability unwrapping 能力解包

在进程间通信（IPC）中，seL4 也可以对能力（capability）进行解包（unwrapping）。如果消息中的第 n 个能力引用了用于发送消息的端点（endpoint），那么该能力会被解包：它的徽章（badge）会被放置在接收者的 IPC 缓冲区的第 n 个位置（在 caps_or_badges 字段中），同时内核会将 seL4_MessageInfo_t 中 capsUnwrapped 字段的第 n 位（从最低有效位开始计数）设置为 1。
解释一下：
在 seL4 系统中，能力（capability）是线程访问系统资源（例如端点、内存等）的权限。在 IPC 通信中，发送方可以通过消息传递这些能力给接收方。解包（unwrapping） 是指内核自动将发送方传递的能力标识符从能力对象中提取出来，并放置在接收方的 IPC 缓冲区中，供接收方使用。
具体来说，如果消息中第 n 个能力引用了用于发送消息的端点（指的是在 IPC 消息中，第 n 个能力是与消息发送的那个端点相关联的能力。换句话说，这个能力能够访问发送消息的端点或者与其进行交互。），那么 seL4 会对这个能力进行特殊处理：它会提取出这个能力的 badge（徽章），并将其放在接收方的 IPC 缓冲区中相应的位置。同时，内核会通过设置 capsUnwrapped 字段中的位来标记哪些能力被解包了。

Message Info

seL4_MessageInfo_t 数据结构用于将 IPC 消息的描述编码为单个字。它用于描述要发送到seL4的消息，并让seL4描述发送到接收者的消息。它包含以下字段：

• length ：消息中消息寄存器（数据）的数量（seL4_MsgMaxLength 最大值）
• extraCaps ：消息中的能力数量 (seL4_MsgMaxExtraCaps)
• capsUnwrapped ：标记被内核解包的能力
• label ：从发送方传输到接收方的未经内核修改的数据

Badges 徽章

除了消息，内核还会传递发送者调用以发送消息的端点能力的徽章（badge）。端点可以通过 seL4_CNode_Mint 或 seL4_CNode_Mutate 来进行标记。一旦端点被徽章标记，接收到该端点消息的任何接收者都会获得该端点的徽章。下面的代码示例演示了这一点：

seL4_Word badge;
seL4_Recv(endpoint, &badge);
// once a message is received, the badge value is set by seL4 to the
// badge of capability used by the sender to send the message

Fastpath

快速 IPC 对于基于微内核的系统至关重要，因为服务通常彼此分离以进行隔离，而 IPC 是客户端和服务之间通信的核心机制之一。因此，IPC 有一个快速路径——内核中经过高度优化的路径——它允许这些操作非常快。为了使用快速路径，IPC 必须满足以下条件：

• 必须使用seL4_Call或seL4_ReplyRecv
• 消息中的数据必须适合 seL4_FastMessageRegisters 寄存器。
• 进程必须具有有效的地址空间
• 不传送能力
• 调度程序中没有比被 IPC 解除阻塞的线程优先级更高的其他线程可以运行。

额，还是想吐槽，太复杂了

实操

这篇教程中有几个由capDL loader设置好的进程，两个clients一个server。所有进程都拥有对同一个端点能力访问的权限，该能力提供了对同一个端点对象的访问。看了上面的背景知识仍然不是很能搞懂，下面插一节补充。

补充

• IPC 缓冲区：每个线程（TCB）都有自己专属的 IPC 缓冲区，用于发送和接收消息。这个缓冲区通常是在线程的用户地址空间内，通过 seL4_SetIPCBuffer 设置。在执行 IPC 操作时，内核会自动将消息放入该线程的 IPC 缓冲区
• 端点（endpoint）：端点是 seL4 中用于线程之间通信的对象。多个线程可以共享同一个端点能力，这意味着它们可以通过这个端点进行通信。例如，两个线程可以都向同一个端点发送或接收消息，从而实现消息的交换或同步

在对端点的解释中，说向同一个端点发送或接收消息，这句话令人很摸不着头脑，下面基于五个对象（线程A、线程B、端点A、线程A的IPC缓冲区、线程B的IPC缓冲区）举一个IPC通信的完整例子，辅助理解。
场景

线程A需要向线程B发送一个消息。线程A和线程B通过端点A来实现通信。每个线程都有自己的IPC缓冲区来存储消息。

对象

• 线程A：发送消息的线程。
• 线程B：接收消息的线程。
• 端点A：线程A 和线程B 用于通信的共享端点。
• 线程A的IPC缓冲区：用于存储线程A发送或接收的消息内容。
• 线程B的IPC缓冲区：用于存储线程B接收的消息内容。

IPC流程

1. 创建端点A： 系统中创建一个端点对象 端点A，它用来作为通信通道，供线程A 和线程B 通过它进行消息的传递。两者共享这个端点。
2. 线程A向端点A发送消息：线程A 将消息放入自己的 IPC缓冲区，并使用系统调用 seL4_Send(endpointA) 来发送消息。这个系统调用会将消息从 线程A的IPC缓冲区 发送到 端点A。端点A 在这个时候相当于一个“信箱”，等待另一个线程（线程B）来取消息。
3. 线程B等待接收消息：线程B 通过调用 seL4_Recv(endpointA) 在 端点A 上等待消息。这时，线程B 阻塞（等待消息到达）。当消息到达时，内核会通过端点讲消息从线程A的IPC缓冲区 拷贝到 线程B的IPC缓冲区。
4. 消息传递完成：当消息被传递到 线程B的IPC缓冲区 后，线程B 不再阻塞，恢复运行，并可以从它的 IPC 缓冲区读取消息。

流程如下：

线程A的IPC缓冲区 ---> 端点A ---> 线程B的IPC缓冲区

上面的流程给人一种端点A存储了通信的信息的感觉，实际上端点A本身并不存储消息。但是它实际上是一个同步机制，用于协调消息在不同线程之间的传递。在seL4中，消息通过IPC机制在不同线程之间传递，端点A起的是“连接”作用，而不是数据存储作用。

IPC的工作机制

• 当 线程A 调用 seL4_Send(endpointA) 发送消息时，消息被存储在线程A的IPC缓冲区中。
• 当 线程B 调用 seL4_Recv(endpointA) 接收消息时，内核会将消息从 线程A的IPC缓冲区 复制到 线程B的IPC缓冲区，通过端点A作为中介来协调消息的传递。
  也就是说，端点A起到的是协调消息传递的作用，它不存储数据，而是促使内核将数据从发送者的缓冲区拷贝到接收者的缓冲区。

所以端点的作用是什么？

• 内核通过它判断哪些线程在等待消息或发送消息。
• 当线程B准备好接收消息时，内核会在后台完成消息从 线程A的IPC缓冲区 到 线程B的IPC缓冲区 的数据拷贝
• 端点A 是一个信号机制，用于确定消息何时可以被传递。它不存储消息，也没有持有对线程A IPC缓冲区的访问权限。

回到教程

在这篇教程中，你将会创建一个服务器，输出由客户端发送过来的信息内容。你还讲更改客户端回复的顺序以获得正确的消息。当你运行代码的时候，输出差不多是这样子的（输出的顺序可能不太一样）：

在初始化时，两个客户端使用以下协议：它们在提供的端点上等待通过能力转移发送给它们的带徽章的端点。之后，客户端发送的所有消息都使用带徽章的端点，以便服务器能够识别客户端。然而，服务器当前并没有发送带徽章的能力！我们提供了代码来给端点能力加徽章，并回复客户端。
练习：我们的任务是设置能力传送，这样客户端才能成功的接收到带徽章的端点（能力）。看一下代码：

seL4_Word badge = seL4_GetMR(0);//这个函数用于从当前线程的消息寄存器中读取指定索引位置的值。索引从 0 开始，因此 seL4_GetMR(0) 返回的是第一个消息寄存器的值。

// server在自己的地址空间复制了一个带徽章的端点能力，下面需要做的是将这个能力传给发送者（看完下面方法的详解就能看懂这个方法是干啥的了）
seL4_Error error = seL4_CNode_Mint(cnode, free_slot, seL4_WordBits,
                                   cnode, endpoint, seL4_WordBits,
                                   seL4_AllRights, badge);
printf("Badged %lu\n", badge);

// TODO use cap transfer to send the badged cap in the reply 将这个徽章标记的端点能力发出去

/* reply to the sender and wait for the next message */
seL4_Reply(info);

/* now delete the transferred cap */
error = seL4_CNode_Delete(cnode, free_slot, seL4_WordBits);
assert(error == seL4_NoError);

/* wait for the next message */
info = seL4_Recv(endpoint, &sender);

看一下seL4_CNode_Mint这个方法，其作用是拷贝一个能力，同时设置其权限和徽章。

现在我们来梳理一下一个server和两个client的逻辑。

对于server.c而言

1. 在初始的时候会调用seL4_Recv阻塞住自己，等待client发送信息过来，在之前我们说过，这个阻塞只要对方有消息过来就会被唤醒
2. 当有消息过来了之后，进入一个死循环，以下是死循环的内容
3. 判断有没有badge。
4. 如果没有badge，则取收到的消息第一个寄存器的内容作为badge，复制一个带badge的endpoint，将能力放在free_slot插槽里面，创建一个IPC消息体，使用reply传回这个消息体，然后删除掉新创建的能力，然后阻塞等待下一条消息（进行下一次循环，回到3）
5. 如果有badge，暂时是空的（指的是原代码，里面的内容需要我们填充），回到3

对于client.c而言（两个client的逻辑完全相同，只挑一个说）

1. 设置好收到的能力放置在哪个槽里面
2. 第一个消息寄存器中填入值
3. 创建一个IPC消息体，使用call发送出去，然后阻塞等待reply
4. 等到了reply之后，将定义在数组中的单词，放置在消息寄存器中发出去，然后阻塞等待回复，直到所有的单词发完为止

上面理清楚了之后做第一个TODO

// TODO use cap transfer to send the badged cap in the reply
// 只发送一个能力
info = seL4_MessageInfo_new(0, 0, 1, 0);
// 消息体的能力槽中指定要传送的能力
seL4_SetCap(0,free_slot);

运行之后输出如下：

运行到这里的时候，两个client都会因为call的调用而阻塞住，而server端因为运行到了else里面，是空的，所以我们需要继续填充else中的内容。
进行下一个TODO：

// TODO use printf to print out the message sent by the client
seL4_Word length = seL4_MessageInfo_get_length(info);//seL4_MessageInfo_get_length这个方法是我搜出来的
for (int i = 0; i <= length; i++)
{
  seL4_Word character = seL4_GetMR(i);  // 获取每个消息寄存器中的字符
  printf("%c", (char)character);   // 将其作为字符打印
}
// followed by a new line
printf("\n");  // 打印换行符

输出如下：

做下一个TODO：

// TODO reply to the client and wait for the next message
//  info = seL4_MessageInfo_new(0, 0, 0, 0);
seL4_Reply(info);
info = seL4_Recv(endpoint, &sender);

输出如下：

不知道为啥报错。 有知道的请留言，seL4_CNode_SaveCaller这个没用，谁用了请留言，交流一下。