ReL4继承和保留了seL4的同步IPC以及异步的Notification，并引入了基于用户态中断的U- notification与异步IPC。

1. 同步IPC #

同步的IPC作为原始的seL4的主要IPC手段，消息的发送方或接收方需要阻塞等待对端的操作，因此并发性相对不足。

同步IPC通过在内核维护一个Endpoint内核对象的状态来实现。Endpoint内部维护了自身的状态以及一个线程阻塞队列，在不同状态上调用不同的系统调用会有不同的行为：

idle：调用Send或Recv都会将src tcb加入阻塞队列。
send：
- 调用Send会将src tcb加入阻塞队列。
- 调用Recv会从阻塞队列头部取出dst tcb并切换到该线程执行。
recv：
- 调用Send会从阻塞队列头部取出dst tcb并切换到该线程执行。
- 调用Recv会将src tcb加入阻塞队列。

内核将Endpoint对应的Capability句柄暴露给用户态，用户态在该句柄上调用Send、Recv、Call或ReplyRecv等系统调用来进行通信。

2. 异步Notification #

由于同步IPC强制用户态使用多线程来实现并发，因此seL4还引入异步的Notification来增强并发的支持。

异步的Notification通过在内核维护一个Notification内核对象的状态来实现。Notification内部维护了了自身的状态、一个信号状态位（badges）以及阻塞队列，在不同状态上调用不同的系统调用会有不同的行为：

idle：
- 调用Signal会将携带的badge参数赋值给对象的badges。
- 调用Wait会将src tcb加入阻塞队列。
waiting：
- 调用Signal会从阻塞队列头部取出dst tcb并切换到该线程执行。
- 调用Wait会将src tcb加入阻塞队列。
Active：
- 调用Signal会将携带的badge参数赋值给对象的badges。
- 调用Wait将badegs参数清空并返回给用户态。

可以看出，与Endpoint的主要区别在于发送端不会阻塞当前线程。

3. U-notification #

即使是异步的Notification依然需要陷入内核去发送和接收用户态中断，陷入内核会造成至少两次特权级的切换，因此对于IPC频繁的应用，特权级的切换将造成大量的系统开销，成为性能瓶颈。因此我们基于用户态中断实现了U-notification。

我们在Notification内核对象中维护了用户态中断的接收方硬件索引，同时还在每个发送线程的TCB中分配了一个发送方的硬件索引。通过新增的系统调用去分配硬件索引，为了保证接口的兼容性，我们用用户态的异步运行时代理了这些分配操作。

U-notification主要分为三个步骤：

注册发送方/接收方：分别通过新增的系统调用实现。
通信：
- 调用Signal：会检查当前线程是否注册发送硬件索引，如果没有，则会先注册，然后调用send_uipi发送用户态中断。
- 调用Wait：会阻塞当前协程，当发送端调用Signal之后，会在中断服务程序中唤醒该协程。
回收：在notification内核对象生命周期结束之后（调用Revoke或Delete）由内核统一进行回收。

4. 异步IPC #

U-notification仅支持少量数据的传输，为了实现任意数据量的IPC，我们在U-notification的基础上，使用共享内存来实现异步IPC。发送端和接收端使用共享内存来进行数据通信，使用U-notification实现同步。

为了更好地封装性和兼容性。我们在用户态提供异步运行时。将每一个用户态任务封装成协程，协程发起IPC请求时会将数据写入共享内存，并发送U-notification进行同步，接收线程会收到U-notification并唤醒接受协程来读取共享内存中的数据。

同时更低限度减少用户态中断的次数，我们设计来自适应的混合轮询机制。我们在共享内存中维护了接收端协程的状态，在发送端发起请求时，会检查接收端协程是否就绪，如果是，则无需发送U-notification。这种机制使得在接收端忙于处理上一个请求时下一个请求已经到来的情况下，尽可能减少用户态中断打断执行流，专注请求的处理。

异步IPC的主要分为四个步骤：

发送端写共享内存
发送端检查接收端状态并发送U-notification。
接收端唤醒接收协程。
接收协程读共享内存。

Interface #

seL4_Send/seL4_NBSend: 阻塞（非阻塞）发送IPC
seL4_Recv/seL4_NBRecv: 阻塞（非阻塞）接收IPC
seL4_Call：阻塞发送IPC并阻塞等待响应。
seL4_ReplyRecv：阻塞发送响应病阻塞等待请求。
seL4_Signal: 发送notification
seL4_Wait: 阻塞接收notification
seL4_Poll: 非阻塞接收notification
reL4_Signal: 发送U-notification
reL4_Wait: 接收U-notification并阻塞当前协程
reL4_Poll：非阻塞接收U-notification
reL4_Send：发送异步，不阻塞当前协程。
reL4_Recv：接收异步IPC，阻塞当前协程。
reL4_Call: 发送异步IPC并阻塞当前协程，等待响应后唤醒。
reL4_ReplyRecv：reL4_Send与reL4_Recv的组合。