RFC-27: Microkit Entrypoint/Deferred API Changes

[midnightveil]

Please see RFC description.

This has been split off from #41 in order to focus these on narrower aspects. There is some relevant discussion there.

View the rendered version here.

[midnightveil]

For time-context, please see the comments prior to this one by me for other discussions. I will edit this comment later to include copies of the relevant sections.

[zaklogician]

With this API, after this return, the next iteration of the handler loop begins, and a conditional is used to invoke NBSendRecv instead of Recv.

If instead of the proposed return types we just had void notified(seL4_Word badge), we could get nigh-identical behavior using

  microkit_irq_ack(...);
  return;

This means that there is no need to introduce these returns types: one can always just rewrite a deferred notify as a "notify before return". At least unless there is a significant and necessary performance advantage to NBSendRecv instead of two calls. One has to benchmark, but I doubt it matters.

If the user wants a specific notify-based-on-returned-value mechanism for some psychological reason, they can always implement it themselves.

[zaklogician]

Note: I do understand that if a PD L calls microkit_notify(..) on a channel that maps to a higher-priority PD H, this may wake H up and cause the kernel to immediately preempt L in order to execute H.

I guess this could lead to measurable performance impact in a situation where H in turn immediately notifies L. But

1. I doubt it
2. the return-type-based solution can also lead to worse performance in various cases, in particular it might introduce an extra branch.

[midnightveil]

The deferred API - and the return API - is all to make use of the ability to do a signal + wait together via NBSendRecv.

I also don't know if it matters, but Gernot definitely wants to use the feature. It would in theory saves cycles, but whether it makes a difference overall, IDK.

The cost of a branch is going to be massively less than the cost of an extra context switch.

[zaklogician]

The cost of a branch is going to be massively less than the cost of an extra context switch.

That's clear, but its not a one-to-one comparison: the branch cost is paid by everybody using Microkit (in parcular all PDs on a system), whereas the extra context switch is fairly niche.

The original reason for introducing deferred wasn't pure performance: it is simply the only way to do certain common things with the current loopy notified api.

[midnightveil]

Offline discussion: proposal from Zoltan is to remove the have_signal branch entirely, the return value can avoid that branch.

The original reason for introducing deferred wasn't pure performance: it is simply the only way to do certain common things with the current loopy notified api.

Right. You previously had to use it if you wanted to only signal once across all the notifies because you didn't know how many times you would be called, leading to over-signalling otherwise.

This was not my understanding of why this was added: see the description in this PR which explicitly states it is for performance: seL4/microkit#183.

[zaklogician]

Nice, that gives perf as the sole justification. Thanks for looking into this. I might do some archeology to try and figure out what the first use cases were, and how they actually affected perf.

[Indanz]

There is no fastpath for NBSendRecv, compared to signal (though not verified), so gain is less than you'd expect.

[Indanz]

The main problem I have with the deferred API is that it either should be done automatically, so users don't need to be aware of it and all code benefits from the optimisation, or not at all.

If you add a Microkit context parameter to all Microkit calls, then you won't need globals and could do deferral transparently.

[dreamliner787-9]

I prefer channel_set.

[dreamliner787-9]

Can't we just provide something like:

typedef uint64_t microkit_channel_set_t;
bool microkit_channelset_is_set(microkit_channel_set_t channel_set, uint64_t channel) {
    return channel_set & (1ul << channel);
}

This way, it is not too bad for Microkit users to adapt the system to the new API. Unless I'm over looking something.

[midnightveil]

Yes we can.