Faults

• 学习什么是线程错误
• 理解线程错误和处理器硬件错误是不同的
• 理解什么是错误处理器
• 理解内核对于一个有错误的线程做了什么
• 了解如何设置内核将在其上传递故障消息的端点（master与 MCS）。
• 在错误故障后学习如何恢复线程。

Background: What is a fault, and what is a fault handler?

故障处理程序是一个单独的指令流，CPU 可以跳转到该指令流以纠正当前线程中的异常情况，然后返回到前一个指令流。
在 seL4 中，故障被建模为由程序员指定的独立“故障处理”线程。在宏内核中，故障通常不会传递给用户空间的处理程序，而是由宏内核本身处理。
一般来说，尝试恢复执行故障线程而不纠正异常只会无限地重新触发故障，直到异常被清除。

Thread faults vs other sources of faults

运行中的系统有多种故障来源；它们包括：

• 当 CPU 在指令流中遇到异常（也称为“处理器异常”）时，CPU 本身会生成故障事件。
• 发生某些硬件异常（例如机器检查或不可屏蔽中断）时，硬件产生的故障事件。
• 当当前线程遇到异常时，seL4 内核生成的故障事件。

本教程仅关注 seL4 内核生成的那些故障事件。从这里开始，我们将把它们称为“线程错误”，以减少歧义。

How does thread fault handling work?

在 seL4 中，当线程生成线程故障时，内核将阻止故障线程的执行，并尝试通过与该线程关联的特殊端点（称为“fault handler”endpoint）传递消息。
故障处理程序端点的唯一特殊之处是一个线程只能拥有其中一个。否则，它的创建和管理方式与任何其他类型的 seL4 端点对象相同。
在故障端点另一端侦听的线程称为“故障处理程序”。内核期望故障处理程序将纠正导致故障线程的异常，然后告诉内核何时可以安全地再次尝试执行故障线程。
要告诉内核恢复故障线程的执行，故障处理程序可以：

• 在故障处理程序端点上调用回复操作（使用seL4_Reply()）并确保seL4_MessageInfo_t标记中的标签设置为0；
• 使用 seL4_TCB_Resume() 明确告诉内核恢复执行故障线程。

请注意，如果处理程序在回复消息中设置消息寄存器，内核可能会将这些解释为某种含义：某些故障回复接受参数。所有故障的回复消息格式请参见seL4手册。
如果故障处理程序没有正确纠正故障线程中的异常，恢复故障线程只会导致内核重新生成故障。

Reasons for thread faults:

线程错误可能因不同的原因而产生。当发生故障时，内核会将描述故障原因的信息作为 IPC 消息传递。在撰写本文时，seL4 内核的 Master 版本可能会产生以下错误：

• 能力故障：由于无效的能力访问而触发的故障。
• VM 故障：页表状态不一致或线程访问内存不正确而引发的故障。
• 未知系统调用故障：通过执行内核未知的系统调用调用而触发。
• 调试故障：当发生断点、观察点或单步调试事件时触发。

此外，MCS内核还添加了以下故障类型：

• 超时错误：当线程消耗完其所有预算并且当前期间仍有进一步执行要做时触发。

Thread fault messages:

当产生故障时，内核将通过故障端点传递 IPC 消息。该 IPC 消息包含告诉故障处理程序发生故障的原因的信息以及有关故障的周围上下文信息，这可能有助于故障处理程序纠正异常。
每个异常都有自己的消息格式，因为描述每个异常所需的信息会有所不同。有关seL4内核针对每个故障异常发送的IPC消息内容的更多信息，请参阅seL4手册。
本教程的其余部分将尝试教读者如何接收和处理 seL4 线程故障。

Setting up a fault endpoint for a thread:

在故障端点上传递故障消息的情况下，内核充当 IPC“发送者”，故障处理程序充当接收者。
这意味着当将能力分配给故障端点对象时，必须给内核分配一个指向该对象的能力，同时也必须给处理程序分配一个指向该对象的能力。

Kernel end vs handler end:

程序员在配置 TCB 时为线程指定使用故障处理程序的能力。因此，程序员还可以在内核能力上为故障端点对象设置一个徽章。
当内核使用带有标记的端点能力发送故障 IPC 消息时，该标记会以与发送方能力上有标记的任何其他 IPC 相同的方式传递到接收方。
敏锐的读者可能已经意识到，这意味着内核的故障端点能力上的标记可用于区分来自不同故障线程的故障消息，以便单个处理程序可以处理来自多个线程的故障。请参阅 IPC 教程，了解带有标记的故障端点的工作原理。

Differences between MCS and Master kernel:

主内核和 MCS 内核之间通知内核故障端点能力的方式存在细微差别。
不管怎样，在两个版本的内核上，要通知内核线程的故障端点，请调用通常的 seL4_TCB_SetSpace()。
有关详细信息，请参阅 MCS 教程。

Exercises

本教程有一个由 CapDL 加载程序设置的地址空间，其中包含共享同一 CSpace 的两个线程。其中一个线程是故障处理程序，而另一个线程则触发虚拟内存故障。
您将被引导完成以下主要步骤：

1. 为故障线程添加标记并配置故障处理程序。
2. 让故障线程触发线程故障。
3. 在故障处理程序中处理故障。
4. 恢复发生故障的线程的执行。

Description of the tutorial program:

本教程介绍了不同虚拟地址空间中的两个线程。一个线程是“故障者”，另一个线程是“处理程序”。错误者将生成错误，处理程序将“处理”它。
为了让处理程序能够处理故障，处理程序必须设置一个故障处理端点，并告诉内核将故障线程生成的所有故障 IPC 消息发送给自己。因此，这是我们采取的第一步。
然而，我们必须确保只有在处理程序线程设置了故障处理端点并准备好从内核接收故障IPC消息之后才会触发故障。
如果故障线程产生故障并且没有线程来处理IPC消息，则内核将简单地挂起故障线程。
因此，我们将故障线程 seL4_call() 设置为跨端点的处理程序线程，并告诉它处理程序应将故障处理端点能力放入哪个槽中。在处理程序设置了处理程序端点后，处理程序将向故障者发送seL4_Reply()，让其知道处理程序已准备好处理故障IPC消息。
之后，我们在错误器中触发错误，在处理程序中处理错误，然后恢复错误器，练习就结束了。

Setting up the endpoint to be used for thread fault IPC messages.（设置用于线程故障IPC消息的端点）

第一个练习是使用故障端点配置故障器的 TCB。这项练习旨在实现两个学习成果：

• 说明提供给内核的端点的末尾可以标记，并且当内核发送故障 IPC 消息时，内核将返回该标记值。
• 解释 Master 内核和 MCS 内核在向内核告知故障端点方面的差异。

现在，故障线程被阻塞在端点上，等待处理程序告诉它将故障处理端点放在它自己的（故障者的）CSpace（对于主内核）中的位置。
为了设置故障处理程序端点，我们首先要对其进行标记，以便当内核向我们发送故障 IPC 消息时，我们将能够识别故障者。故障处理程序可以处理来自多个线程的故障，因此徽章使处理程序能够识别他们正在处理的故障程序。
要标记端点，请使用 seL4_CNode_Mint() 系统调用：

error = seL4_CNode_Mint(
        handler_cspace_root,
        badged_faulter_fault_ep_cap,
        seL4_WordBits,
        handler_cspace_root,
        faulter_fault_ep_cap,
        seL4_WordBits,
        seL4_AllRights, FAULTER_BADGE_VALUE);

由于我们使用的是 Master 内核，因此您还需要将标记能力复制到故障者的 CSpace 中（有关配置故障端点时 Master 和 MCS 内核之间差异的说明，请参阅 MCS 教程）：

 error = seL4_CNode_Copy(
        faulter_cspace_root,
        foreign_badged_faulter_empty_slot_cap,
        seL4_WordBits,
        handler_cspace_root,
        badged_faulter_fault_ep_cap,
        seL4_WordBits,
        seL4_AllRights);

最后，我们告诉内核故障端点的能力地址，以便内核可以将故障IPC消息传递给处理程序。由于我们使用的是 Master 内核，因此我们需要传递一个可以从错误线程的 CSpace 中解析的 CPtr：

error = seL4_TCB_SetSpace(
        faulter_tcb_cap,
        foreign_badged_faulter_empty_slot_cap,
        faulter_cspace_root,
        0,
        faulter_vspace_root,
        0);

简单来说上面的流程就是，先使用Mint方法复制一个端点能力，并赋予其徽章。然后使用copy方法将这个带徽章的能力复制到故障者的CSpace中，然后设置这个线程的故障端点、CSpace以及VSpace（当然这两个没有改变）。
为什么还能改变线程的能力空间和虚拟地址空间呢？虽然线程可能已经有一个 CSpace，但是 seL4_TCB_SetSpace 是用来显式地重新绑定或确认 CSpace 的根节点。在某些情况下，可能希望改变线程的 CSpace，或者确保线程可以在不同的能力空间上下文中执行。VSpace 代表线程的地址空间布局。当你调用 seL4_TCB_SetSpace 时，通过设置这个参数，你明确指定该线程使用哪个 VSpace。虽然在初始化线程时已经绑定了 VSpace，但在某些场景下可能需要更改它。例如，在虚拟化环境中，某些线程可能需要切换到不同的虚拟地址空间（不同的 VSpace）以访问不同的内存布局，或者在权限变化时需要重新指定 VSpace。

Receiving the IPC message from the kernel:

内核将会给等待在故障端点上的所有线程传递IPC消息。使用seL4_Recv()阻塞等待IPC消息，同样也可以用于等待其他的IPC消息：

foreign_faulter_capfault_cap = seL4_GetMR(seL4_CapFault_Addr);

Finding out information about the generated thread fault:

在线程故障IPC消息中，内核将发送有关故障的信息，包括访问触发线程故障的能力地址。 seL4 手册提供了有关 IPC 缓冲区中哪些消息寄存器包含有关故障的信息的详细信息，如果您愿意，libsel4 源代码也有确切的代码值。
在我们这里的示例中，我们的示例代码生成了一个 Cap 错误，因此根据 seL4 手册，我们可以使用 IPC 消息中的偏移量 seL4_CapFault_Addr 找到 Cap 错误地址，如上面的代码片段所示。所以，you know，seL4_CapFault_Addr 是已经定义好的常量。

Handling a thread fault:

现在我们知道了在故障线程中生成故障的能力地址，我们可以通过将随机能力放入该插槽来“处理”故障，然后当故障线程重新尝试访问该插槽时，这次它将成功并且不会产生线程错误。
因此，在这里我们将端点能力复制到故障槽中：

error = seL4_CNode_Copy(
        faulter_cspace_root,
        foreign_faulter_capfault_cap,
        seL4_WordBits,
        handler_cspace_root,
        sequencing_ep_cap,
        seL4_WordBits,
        seL4_AllRights);

Resuming a faulting thread:

最后，为了唤醒故障线程并尝试再次执行，我们对其进行 seL4_Reply() ：

seL4_Reply(seL4_MessageInfo_new(0, 0, 0, 0));

贴出来handler的代码

#include <assert.h>
#include <stdio.h>
#include <sel4/sel4.h>
#include <utils/util.h>
#include <autoconf.h>

#define FAULTER_BADGE_VALUE     (0xBEEF)
#define PROGNAME                "Handler: "
/* We signal on this notification to let the fauler know when we're ready to
 * receive its fault message.
 */
extern seL4_CPtr sequencing_ep_cap;

extern seL4_CPtr faulter_fault_ep_cap;

extern seL4_CPtr handler_cspace_root;
extern seL4_CPtr badged_faulter_fault_ep_cap;

extern seL4_CPtr faulter_tcb_cap;
extern seL4_CPtr faulter_vspace_root;
extern seL4_CPtr faulter_cspace_root;

int main(void)
{
    int error;
    seL4_Word tmp_badge;
    seL4_CPtr foreign_badged_faulter_empty_slot_cap;
    seL4_CPtr foreign_faulter_capfault_cap;
    seL4_MessageInfo_t seq_msginfo;

    printf(PROGNAME "Handler thread running!\n"
           PROGNAME "About to wait for empty slot from faulter.\n");


    seq_msginfo = seL4_Recv(sequencing_ep_cap, &tmp_badge);
    foreign_badged_faulter_empty_slot_cap = seL4_GetMR(0);
    printf(PROGNAME "Received init sequence msg: slot in faulter's cspace is "
           "%lu.\n",
           foreign_badged_faulter_empty_slot_cap);



    /* Mint the fault ep with a badge */

    error = seL4_CNode_Mint(
        handler_cspace_root,
        badged_faulter_fault_ep_cap,
        seL4_WordBits,
        handler_cspace_root,
        /* EXERCISE: Which capability should be the source argument here? */faulter_fault_ep_cap,
        seL4_WordBits,
        seL4_AllRights, FAULTER_BADGE_VALUE);

    ZF_LOGF_IF(error != 0, PROGNAME "Failed to mint ep cap with badge!");
    printf(PROGNAME "Successfully minted fault handling ep into local cspace.\n");


    /* This step is only necessary on the master kernel. On the MCS kernel it
     * can be skipped because we do not need to copy the badged fault EP into
     * the faulting thread's cspace on the MCS kernel.
     */

    error = seL4_CNode_Copy(
        faulter_cspace_root,
        /* EXERCISE: What should the destination be for this cap copy? */foreign_badged_faulter_empty_slot_cap,
        seL4_WordBits,
        handler_cspace_root,
        badged_faulter_fault_ep_cap,
        seL4_WordBits,
        seL4_AllRights);

    ZF_LOGF_IF(error != 0, PROGNAME "Failed to copy badged ep cap into faulter's cspace!");
    printf(PROGNAME "Successfully copied badged fault handling ep into "
           "faulter's cspace.\n"
           PROGNAME "(Only necessary on Master kernel.)\n");

    error = seL4_TCB_SetSpace(
        faulter_tcb_cap,
        foreign_badged_faulter_empty_slot_cap,
        faulter_cspace_root,
        0,
        faulter_vspace_root,
        0);
    seL4_Reply(seL4_MessageInfo_new(0, 0, 0, 0));
    // handler阻塞等待在自己的badged端点上面
    seL4_Recv(badged_faulter_fault_ep_cap,&tmp_badge);

    foreign_faulter_capfault_cap = seL4_GetMR(seL4_CapFault_Addr);

    error = seL4_CNode_Copy(
        faulter_cspace_root,
        foreign_faulter_capfault_cap,
        seL4_WordBits,
        handler_cspace_root,
        sequencing_ep_cap,
        seL4_WordBits,
        seL4_AllRights);
    seL4_Reply(seL4_MessageInfo_new(0, 0, 0, 0));
    return 0;
}

最后输出如下：