seL4 Notifications（六）

Notification

理解如何在任务之间设置共享内存
能够使用通知对象在任务之间进行同步
理解如何使用徽章进行通知区分

Background

通知允许进程发送异步信号给彼此，主要用于中断处理以及同步访问共享数据缓存。

信号量对象

信号是通过能力上的调用进行发送和接收到通知对象的。一个通知对象由一个数据字以及一个等待通知的TCB队列组成，该数据字充当二进制信号量数组。

通知对象有三种状态：

Waiting ，有TCBs队列等待在该通知上等待被唤醒
Active，TCBs已就该通知发出了数据
Idle ，没有 TCB 排队，并且自上次设置为空闲以来没有 TCB 向该对象发出信号

Signalling

当任务通过 seL4_Signal 向一个通知对象发出信号时，发生的情况取决于该通知对象的状态：

Idle，数据字被设置为用于发送信号的能力的徽章，并且对象被转换为active
Active，用于向通知对象发出信号的能力徽章与通知数据字按位或运算
Waiting，TCB 队列的头被唤醒，并将徽章发送到该 TCB。如果队列为空，则通知对象将转换为空闲状态。

通过这种方式，通知对象可以被视为信号量的二进制数组——如果信号发送者都在徽章中使用不同的位来发送信号，则他们可以设置不同的徽章位，并且等待者可以观察已设置哪些位。

Waiting

任务可以使用 seL4_Wait 等待通知对象，它执行以下操作：

Idle，如果任务处于空闲状态，TCB（任务控制块）会被加入队列，通知对象的状态会变为“等待”状态。
Active，如果任务处于活动状态，TCB 会收到数据字，数据字会被重置为 0，同时通知对象的状态会变为“空闲”。
Waiting，如果任务处于等待状态，TCB 会被附加到队列中。

Polling

通知对象还可以使用 seL4_Poll 进行轮询，seL4_Poll 是 seL4_Wait 的非阻塞版本，无论状态如何都会立即返回。

Interrupts and IPC

通知对象可以用来接收中断传递的信号，也可以绑定到TCB，使得信号和IPC可以由同一个线程接收。定时器教程对此进行了更详细的解释。

练习

这些练习将指导您完成使用通知和共享内存设置的基本生产者消费者。本教程使用 capDL 加载程序，并且已经有 2 个生产者进程（生产者_1.c 和生产者_2）和 1 个正在运行的消费者进程（consumer.c）。每个进程都可以使用许多能力。
每个生产者与消费者共享一个缓冲区，消费者在来自两个生产者的数据可用时处理该缓冲区。当您开始本教程时，输出将如下所示：

Booting all finished, dropped to user space
Waiting for producer

Set up shared memory

两个生产者都立即启动并阻塞，等待消费者发送带有共享映射地址的 IPC。我们提供下面的代码来设置生产者 1 和消费者之间的共享页：

    /* 复制能力，将cnode->buf1_frame_cap这个能力复制到cnode->mapping_1这个里面，槽位大小为seL4_WordBits，权限为全部*/error = seL4_CNode_Copy(cnode, mapping_1, seL4_WordBits, cnode, buf1_frame_cap, seL4_WordBits, seL4_AllRights);ZF_LOGF_IFERR(error, "Failed to copy cap");/*将物理帧映射到虚拟地址，将mapping_1能力表示的物理帧映射到producer_1_vspace中，从BUF_VADDR这里开始映射，所有权限默认属性*/error = seL4_ARCH_Page_Map(mapping_1, producer_1_vspace, BUF_VADDR, seL4_AllRights, seL4_ARCH_Default_VMAttributes);ZF_LOGF_IFERR(error, "Failed to map frame");

为什么在进行物理帧映射时需要复制能力（capability）？
当复制一个能力时，可以为新的能力指定不同的权限。在 seL4_CNode_Copy 中，你可以指定不同的访问权限（如只读或读写）。这种操作有助于在不同的上下文中使用该帧时施加不同的访问控制。可以细粒度的分场景控制访问权限进行能力的管理和隔离。
一个物理帧通常需要被多个不同的虚拟地址空间映射，这在内存共享等场景下非常常见。通过复制能力，每个映射都可以有独立的能力实例，这样可以追踪、管理和撤销每个映射，而不会影响其他映射。例如，如果你想取消某个特定映射，只需要撤销该映射的能力，而不会影响原始的 buf1_frame_cap 或其他复制的能力。

给的consumer.c中只进行了第一个映射（consumer.c和producer1.c），没有进行第二个映射。下面做第二个映射：

	error = seL4_CNode_Copy(cnode, mapping_2, seL4_WordBits, cnode, buf2_frame_cap, seL4_WordBits, seL4_AllRights);ZF_LOGF_IFERR(error, "Failed to copy cap");error = seL4_ARCH_Page_Map(mapping_2, producer_2_vspace, BUF_VADDR, seL4_AllRights, seL4_ARCH_Default_VMAttributes);ZF_LOGF_IFERR(error, "Failed to map frame");

当消费者访问他们的缓冲区时，这是否成功将在下一次练习后可见。如果生产者 2 的共享页面设置不正确，它将因虚拟机故障而失败。

Signal the producers to go

此时，两个生产者都在等待空通知，以获取缓冲区已准备好写入的信号。
练习：通过 buf1_empty 和 buf2_empty 通知对象向两个生产者发出信号。
这里在OS的书里面可以学习到，就是生产者和消费者需要两个信号量，一个full一个empty，然后对二者进行pv操作，来协调生产消费。

// TODO signal both producers,唤醒等待在这两个信号量上的线程seL4_Signal(buf1_empty);seL4_Signal(buf2_empty);

Differentiate signals

唤醒之后的输出如下：
在这里插入图片描述
此时，消费者应该使用适当缓冲区中的数据，并向适当消费者发出缓冲区再次为空的信号。完整通知对象的功能已标记： Producer_1 副本的标记为 0b1， Producer_2 的标记为 0b10。通过检查徽章中的位，您可以看到哪个生产者（可能是两个）生产了数据。
练习：检查徽章并根据徽章值中设置的位向生产者发出empty通知信号。

// TODO, use the badge to check which producer has signalled you, and signal it back. Note that you // may recieve more than 1 signal at a time.if(badge == 1){seL4_Signal(buf1_empty);}else if(badge == 2){seL4_Signal(buf2_empty);}else{seL4_Signal(buf1_empty);seL4_Signal(buf2_empty);}