proto-rfc: the microkit API shouldn't exist (mostly)

[midnightveil]

Or, at the very least, we should stop adding more functions to its API. ¹

To be clear, this is my opinion, and for discussion.

the issue

Currently, the microkit API includes functions like:

static inline void microkit_notify(microkit_channel ch)
{
    seL4_Signal(BASE_OUTPUT_NOTIFICATION_CAP + ch);
}

static inline seL4_Word microkit_msginfo_get_count(microkit_msginfo msginfo)
{
    return seL4_MessageInfo_get_length(msginfo);
}

static inline void microkit_mr_set(seL4_Uint8 mr, seL4_Word value)
{
    seL4_SetMR(mr, value);
}

static inline seL4_Word microkit_mr_get(seL4_Uint8 mr)
{
    return seL4_GetMR(mr);
}

In my opinion, why? This is, in my opinion, a prime example of a leaky abstraction.

There are some good parts:

• You don't need to deal with seL4 capabilities, one of the most confusing parts.
• The API surface area (was) massively reduced.

However, it abstracts something so... simple it seems to have no point. The only thing it does is error handling (by... panicking) and translation of the "channel ID" to the actual cap ID.

Where this falls apart a bit more, is using APIs not exposed by microkit: for instance, anything that wants to be a fault() handler tends to want to call seL4_TCB_ReadRegisters (and write), but this isn't implemented: instead it gets called directly: https://github.com/au-ts/libvmm/blob/8f0665dea882130bb5f25311dcd47a1500d80ffe/src/arch/aarch64/fault.c#L264-L280. The same thing with other fault information. Our sDDF "os abstraction" for notifications so that sDDF can work on other seL4 systems that aren't microkit needs to add another layer of abstraction, e.g.: https://github.com/au-ts/sddf/blob/81424f047b09363a1f9f95d293a51167f6403859/include/microkit/os/sddf.h#L31-L34.

In the end, the microkit API either needs to extend to the entire seL4 API, (at a loss of use for non-microkit seL4 libraries) or users need to poke at the internal cap layout. Hence, a "leaky abstraction".

Whilst there can be benefit to "a simpler API" to make it easier for people to start writing microkit systems without understanding seL4's entire capability API, in the end we have a limited form of capabilities: the opaque channel or vcpu IDs that are then translated internally. But most of the wrappers do barely more than take the ID, add an offset, then call the seL4 API. I don't think it really makes sense to

an alternative

Most microkit examples look something like this:

#define CHANNEL_IRQ     0
#define CHANNEL_ANOTHER 1

void init(void) {
    microkit_notify(CHANNEL_ANOTHER);
}

void notified(microkit_ch ch) {
    switch (ch) {
        case CHANNEL_IRQ:
            // handle IRQ
            microkit_irq_ack(CHANNEL_IRQ);
            break;
        case CHANNEL_ANOTHER:
            // do something
            break;
    }
}

The alternative: convey this information in the channel and use seL4 APIs directly. This way you don't need to care about the capability layout,

// this would in essence do the BASE_CHANNEL_CAP + num
#define CHANNEL_IRQ new_channel(0)
#define CHANNEL_ANOTHER new_channel(1)

void init(void) {
    seL4_Signal(CHANNEL_ANOTHER);
}

Then, you still get the "simple" numbers without dealing with capabilities, but you can still call any of the seL4 APIs that use these capabilities directly. (We can also be backwards compatible since we know the internals). The one change would be in notified/etc ² where we probably want to keep passing the channel ID, and then people can construct the actual "channel obj" from this.

This also maps well with the rust-style, which uses const IRQ: Channel = Channel::new(0).

This abstraction isn't leaky (I hope; it's at least significantly less leaky): what the microkit tool is doing is much closer to setting up the capability layout than being a whole new seL4 API.

Doing this means the TCB_ReadRegisters can be done on the TCB_CHILD_1 directly, it's the "standard" way of doing this.

I don't think it's worth trying to hide what the actual API is doing in the end, when often you need to escape anyway. And I don't think it's worth the effort wrapping the entire seL4 API underneath, when you can expose a thin wrapper over the underlying seL4 abstractions which do exist, making up something fairly different seems like a bad idea.

Footnotes

1. The one case where it does make sense to have an API though, is for things like the microkit_name symbol. ↩

2. I want to change this anyway... in my opinion notified should return a channel, rather than void; this would map better onto what the libmicrokit needs to do instead of passing it back instead via this microkit_deferred_signal API. ↩

[Indanz]

I fully agree with this and I always wondered why it is like it is, especially because you really want to use the register-only versions of the IPC functions instead of always going via the IPC buffer.

Long-term, seL4 is very suitable to connect multiple blocks together, because it has a clear and nice abstraction via capabilities. Main thing missing is an agreed way of doing message passing via shared memory, that needs to be abstracted away or agreed on the same mechanism, like following sDDF.

The main difficulty of seL4 is capability space management and the tediousness of launching applications, not the actual call and notification API itself.

Also, you can easily keep the existing wrappers for backward compatibility.