sel4源码解析（四） - ipc

sel4提供了基于endpoints实现的进程间通信，用于进程之间发送少量的信息和cap。

ipc相关数据结构

ipc是通过内核endpoints实现的，相应的有endpoints的结构体和endpoints cap的结构体。endpoints类似notification都有一个队列保存着当前挂载的队列，但endpoints同notification不同，notification是用来发送通知，并没有携带信息和cap。具体结构体如下所示：

block endpoint {
    field epQueue_head 64
    padding 16
    field_high epQueue_tail 46
    field state 2
}

block endpoint_cap(capEPBadge, capCanGrantReply, capCanGrant, capCanSend,
                   capCanReceive, capEPPtr, capType) {
    field capEPBadge 64

    field capType 5
    field capCanGrantReply 1
    field capCanGrant 1
    field capCanReceive 1
    field capCanSend 1
    padding 7
    field_high capEPPtr 48
}

内核函数

void sendIPC(bool_t blocking, bool_t do_call, word_t badge, bool_t canGrant, bool_t canGrantReply, tcb_t *thread, endpoint_t *epptr)
void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
void cancelIPC(tcb_t *tptr)

ipc 流程

为了简单起见，我们举了一个简单但非常实用的例子：有两个进程，一个进程发送信息，另外一个进程接收信息。具体流程如下：

1. 双方进程申请endpoint，得到endpoint的cap。两个进程的cap是同一个cap，该方法由sel4提供的capdl（capability description language）实现；
2. 进程1执行seL4_Send，该函数从ipc buffer里面取出数据放到寄存器x2-x5里，并发起系统调用；
3. 然后执行sendIPC函数，该函数判断endpoint的状态，此时为idle状态（还没有进程在endpoint处等待），且blocking为True。故将当前进程1挂载到endpoint的队列上，置endpoint的状态为send状态；
4. 进程2执行seL4_Recv，发起系统调用；
5. 然后执行receiveIPC函数，该函数判断endpoint的状态，此时为send状态（说明进程需要的信息已经发出了）。故将endpoint的队列取出进程1，读取发送的message和badge给进程2；
6. 完成。