sel4_ipc_optimization.c

#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>

#define _assert_fail(msg, ...) do { puts(msg); exit(1); } while (0)
#define CONST   __attribute__((__const__))
#define seL4_Null   ((void*)0)
#define LIBSEL4_INLINE_FUNC static inline
typedef uint32_t seL4_CPtr;
typedef uint32_t seL4_Word;
typedef uint32_t seL4_MessageInfo_t;

typedef enum {
    seL4_SysSend = -3,
} seL4_Syscall_ID;

typedef struct seL4_IPCBuffer_ {
    seL4_Word msg[32];
} seL4_IPCBuffer __attribute__((__aligned__(sizeof(struct seL4_IPCBuffer_))));

__thread seL4_IPCBuffer *__sel4_ipc_buffer;

LIBSEL4_INLINE_FUNC seL4_IPCBuffer *seL4_GetIPCBuffer(void)
{
    return __sel4_ipc_buffer;
}

LIBSEL4_INLINE_FUNC seL4_Word seL4_GetMR(int i)
{
    return seL4_GetIPCBuffer()->msg[i];
}

LIBSEL4_INLINE_FUNC void seL4_SetMR(int i, seL4_Word mr)
{
    seL4_GetIPCBuffer()->msg[i] = mr;
}

static inline void riscv_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1,
                                  seL4_Word mr2, seL4_Word mr3)
{
    register seL4_Word destptr asm("a0") = dest;
    register seL4_Word info asm("a1") = info_arg;

    /* Load beginning of the message into registers. */
    register seL4_Word msg0 asm("a2") = mr0;
    register seL4_Word msg1 asm("a3") = mr1;
    register seL4_Word msg2 asm("a4") = mr2;
    register seL4_Word msg3 asm("a5") = mr3;

    /* Perform the system call. */
    register seL4_Word scno asm("a7") = sys;
    asm volatile(
        "ecall"
        : "+r"(destptr), "+r"(msg0), "+r"(msg1), "+r"(msg2),
        "+r"(msg3), "+r"(info)
        : "r"(scno)
    );
}

static inline seL4_MessageInfo_t __attribute__((__const__))
seL4_MessageInfo_new(uint32_t label, uint32_t capsUnwrapped, uint32_t extraCaps, uint32_t length) {
    seL4_MessageInfo_t seL4_MessageInfo;

    /* fail if user has passed bits that we will override */
    if(!((label & ~0xfffffu) == ((0 && (label & (1u << 31))) ? 0x0 : 0))) _assert_fail("(label & ~0xfffffu) == ((0 && (label & (1u << 31))) ? 0x0 : 0)", "/home/seiya/NeptuneOS/build-i386-debug/elf/kernel/generated/sel4/shared_types_gen.h", 94, __FUNCTION__);
    if(!((capsUnwrapped & ~0x7u) == ((0 && (capsUnwrapped & (1u << 31))) ? 0x0 : 0))) _assert_fail("(capsUnwrapped & ~0x7u) == ((0 && (capsUnwrapped & (1u << 31))) ? 0x0 : 0)", "/home/seiya/NeptuneOS/build-i386-debug/elf/kernel/generated/sel4/shared_types_gen.h", 95, __FUNCTION__);
    if(!((extraCaps & ~0x3u) == ((0 && (extraCaps & (1u << 31))) ? 0x0 : 0))) _assert_fail("(extraCaps & ~0x3u) == ((0 && (extraCaps & (1u << 31))) ? 0x0 : 0)", "/home/seiya/NeptuneOS/build-i386-debug/elf/kernel/generated/sel4/shared_types_gen.h", 96, __FUNCTION__);
    if(!((length & ~0x7fu) == ((0 && (length & (1u << 31))) ? 0x0 : 0))) _assert_fail("(length & ~0x7fu) == ((0 && (length & (1u << 31))) ? 0x0 : 0)", "/home/seiya/NeptuneOS/build-i386-debug/elf/kernel/generated/sel4/shared_types_gen.h", 97, __FUNCTION__);

    seL4_MessageInfo = 0
        | (label & 0xfffffu) << 12
        | (capsUnwrapped & 0x7u) << 9
        | (extraCaps & 0x3u) << 7
        | (length & 0x7fu) << 0;

    return seL4_MessageInfo;
}

static inline uint32_t CONST
seL4_MessageInfo_get_length(seL4_MessageInfo_t seL4_MessageInfo) {
    uint32_t ret;
    ret = (seL4_MessageInfo & 0x7fu) >> 0;
    /* Possibly sign extend */
    if (__builtin_expect(!!(0 && (ret & (1u << (31)))), 0)) {
        ret |= 0x0;
    }
    return ret;
}

LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
                                          seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
    riscv_sys_send(seL4_SysSend, dest, msgInfo,
                   mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
                   mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
                   mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
                   mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
    );
}

LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
    riscv_sys_send(seL4_SysSend, dest, msgInfo, seL4_GetMR(0), seL4_GetMR(1),
                   seL4_GetMR(2), seL4_GetMR(3));
}

// 本書で紹介したメッセージ送信ロジック
int main(void) {
    seL4_CPtr dest = 123 /*  適当な値 */;
    seL4_MessageInfo_t msgInfo = seL4_MessageInfo_new(0, 0, 0, 4);
    seL4_SetMR(0, 1000);
    seL4_SetMR(1, 1001);
    seL4_SetMR(2, 1002);
    seL4_SetMR(3, 1003);
    seL4_Send(dest, msgInfo);
    return 0;
}

// seL4_SendWithMRs を使ったメッセージ送信ロジック
int main_with_seL4_SendWithMRs(void) {
    seL4_CPtr dest = 123 /*  適当な値 */;
    seL4_MessageInfo_t msgInfo = seL4_MessageInfo_new(0, 0, 0, 4);
    seL4_Word mr0 = 1000;
    seL4_Word mr1 = 1001;
    seL4_Word mr2 = 1002;
    seL4_Word mr3 = 1003;
    seL4_SendWithMRs(dest, msgInfo, &mr0, &mr1, &mr2, &mr3);
    return 0;
}