Skip to content

RFC-26: Microkit API/Entrypoint Changes - #41

Open
midnightveil wants to merge 1 commit into
seL4:mainfrom
au-ts:julia/microkit-api-changes
Open

RFC-26: Microkit API/Entrypoint Changes#41
midnightveil wants to merge 1 commit into
seL4:mainfrom
au-ts:julia/microkit-api-changes

Conversation

@midnightveil

@midnightveil midnightveil commented Aug 6, 2026

Copy link
Copy Markdown

Please see RFC description.

View the rendered version here.

Related: seL4/microkit#526, seL4/microkit#510, seL4/microkit#362.

Things to fix:

  • the code highlighting is broken
  • in one section I don't end a paragraph
  • should mention verification updates in the drawbacks (although Zoltan has said it would make it easier for the notified change)

Please see RFC description.

Signed-off-by: Julia Vassiliki <[email protected]>
@Indanz

Indanz commented Aug 6, 2026

Copy link
Copy Markdown
Contributor

Summary of proposed changes as I understood it, for SDF:

  • Add types to channels to make explicit what kind of channel it is.
  • Split ID into send/recv with allowance for duplicate receive IDs, to make it possible to group multiple channels together under the same ID, to bypass the 63 limit.

For runtime API:

  • notified takes a bitmask instead of being called per ID.
  • Add microkit_ntfn_cap(), etc. wrapper functions making it possible to do direct libsel4 calls and removing Microkit's wrapper functions.
  • Return deferred signal info instead of passing it via global variables.

The 63 bit limit will still be there, but only for receiving notifications. So one server still can't receive from more than 63 clients if it wants to distinguish the notifier. This is a kernel limitation. For calls, Microkit added an artificial limitation which can be removed.

I am a bit confused why an API change is needed though, lumping signals and calls together is an implementation details. Splitting that up doesn't need to be visible in the API I think? The only limitation is that all notification channels must be < 64 and you can't enforce that at build time because you miss the information. But it's easy enough to enforce at runtime.

Adding a new notified entry point that takes a channel set should be easy enough, just implement a weakly linked version of it that calls the old notified in a loop. Same for the ability of the user to call seL4_Signal directly: Just add microkit_ntfn_cap() and microkit_ep_cap() functions. But forcing a big API change without direct advantages for the user doesn't seem the way to go.

I think the current deferred API is more pain than gain. Returning the data is an improvement, but clunky to use. Delegation to other functions is harder then. Have you considered adding a pointer to the struct as an extra parameter instead? Then the user needs to pass that to the new deffer function, but the API is otherwise the same.

You can make the old deferred functions dummy functions that immediately send the signal without deferral, with a deprecation warning. That at least doesn't directly break the user code.

Channel types can also be added as an optional attribute to the existing channel element.

The whole channel concept as it currently exists is a bit awkward because it seems symmetric by default. Splitting receive IDs and send IDs is a bit of a work-around for that. The same could be achieved by allowing the same PD to be listed in a channel multiple times: Then you can add the receive-only duplicate one by specifying notify=false (and a duplicate=true if you want to distinguish between accidental and deliberate ID clashes, or make that the default behaviour for recv-only ones).

What might be better than duplicate IDs, is to explicitly allow more than 2 PDs in a channel, because that's what you're trying to achieve anyway. You're just missing an attribute which says that a PD isn't a sender. Receive-only you do with notify=false, but you need a receive_notify=false to get what you're trying to achieve. And then enforce that in a given set of PDs in a channel, there is either only one sender or only one receiver.

This would make more sense to me conceptually, because the send side is a different channel than the receive side. Instead of binding multiple channels together via duplicate IDs into virtually one channel, you explicitly create a new asymmetric channel directly.

The old example system doesn't match the new one, which is not helpful. If you want to introduce new features, add them later separately, but don't lump it with the old versus new syntax examples.

@midnightveil

Copy link
Copy Markdown
Author

Adding a new notified entry point that takes a channel set should be easy enough, just implement a weakly linked version of it that calls the old notified in a loop. Same for the ability of the user to call seL4_Signal directly: Just add microkit_ntfn_cap() and microkit_ep_cap() functions. But forcing a big API change without direct advantages for the user doesn't seem the way to go.

Yes, like I said we can backcompat that one pretty easily. However I don't necessarily want to keep backcompat features around forever, and not all languages support weak symbols.

There are advantages for the user with new APIS, e.g....

I think the current deferred API is more pain than gain. Returning the data is an improvement, but clunky to use. Delegation to other functions is harder then. Have you considered adding a pointer to the struct as an extra parameter instead? Then the user needs to pass that to the new deffer function, but the API is otherwise the same.

The new deferred API via return relies on the notified bitmask changes. Notably; the fact that we only call notified() once is important for a return value to make sense - structurally this enforces "do one thing at the end".

I disagree that it's clunky; the clinkiest part is constructing the tagged enum because it's C. Passing the return value as a pointer would technically work, too, it is what fault() does. It also relies on the single-notified-call property. I dislike passing return value as a pointer as (a) we have less than 64 bits of information necessary in the return anyway, and (b) it forces loads/stores from the stack, and there's no prevention against writing to it many times. A user can always declare their own stack variable and return it later; they cannot declare their own return value instead of using the pointer argument.

What might be better than duplicate IDs, is to explicitly allow more than 2 PDs in a channel, because that's what you're trying to achieve anyway. You're just missing an attribute which says that a PD isn't a sender. Receive-only you do with notify=false, but you need a receive_notify=false to get what you're trying to achieve. And then enforce that in a given set of PDs in a channel, there is either only one sender or only one receiver.

Yes, this might be a nicer way to represent this in the SDF, I was not entirely convinced with my proposal.

One issue with this proposal is that not splitting ny types in some way retains the existing property that channel IDs for notifications and PPCs are shared. In theory it is possible to not report conflicts if not necessary, e.g.

<channel>
  <end id="0" pd="a" notify=yes ppc=no />
  <end id="0" pd="b" />
</channel>
// and

<channel>
  <end id="0" pd="a" notify=no ppc=yes />
 <end id="0" pd="c" />
</channel>

Would not conflict at all. This seems... confusing. I'm not sure if my proposal actually improves on it much, but having the "type" of a channel just be an attribute on a particular ID implies that IDs are global across channel types.
Would not conflict or indeed

This would make more sense to me conceptually, because the send side is a different channel than the receive side. Instead of binding multiple channels together via duplicate IDs into virtually one channel, you explicitly create a new asymmetric channel directly.

But I do like this, so I could integrate this into my split-per-type channel suggestion; since notably this doesn't work for ppcs, only notifications.

The old example system doesn't match the new one, which is not helpful. If you want to introduce new features, add them later separately, but don't lump it with the old versus new syntax examples.

Can separate, I just wanted to comment on how those fit with the story. (they haven't changed syntax).

I am a bit confused why an API change is needed though, lumping signals and calls together is an implementation details. Splitting that up doesn't need to be visible in the API I think? The only limitation is that all notification channels must be < 64 and you can't enforce that at build time because you miss the information. But it's easy enough to enforce at runtime

Technically, no, this could be two separate changes. However, the existing API and the way notified works strongly implies the assumptions about channel IDs (global across channel types, 1:1 between sender & receiver, etc).

@Indanz

Indanz commented Aug 7, 2026

Copy link
Copy Markdown
Contributor

Yes, like I said we can backcompat that one pretty easily. However I don't necessarily want to keep backcompat features around forever, and not all languages support weak symbols.

It doesn't matter if other languages don't support it, as long as libmicrokit has the symbol marked weakly linked. But I just found out that weak symbols are not standardised, but toolchain dependent, oh joy.

The new deferred API via return relies on the notified bitmask changes. Notably; the fact that we only call notified() once is important for a return value to make sense - structurally this enforces "do one thing at the end".

But this assumes that everything happens in the notified function, which in reality won't be the case except for very simple programs.

For any somewhat structured code, different notifications would be handled by calling different functions, and those are the ones that sometimes may want to do a deferred signal. Those different functions shouldn't need to be aware of each other. Doing deferral via return values is very awkward to do then.

In your example there is no reason not to do a deferred call for NTFN_PD_B. But that only works if CH_PDS isn't set. And what if there are 5 other cases, what then? How do you want to combine multiple, independent modules of code with this API?

(And it doesn't matter that the current API doesn't support it and would consider that a bug. That's just a bad API that can easily be fixed by flushing pending signals instead of losing them.)

While if you pass a pointer, you can use the existing deferral API and automatically flush if there already is anything pending. Then the API is simple to use and robust. All state is handled in one place, with no tricky or annoying code for users to deal with.

All in all it seems that the current API is a better fit for the deferred stuff than the bitmask version.

I disagree that it's clunky; the clinkiest part is constructing the tagged enum because it's C.

But having it as a return value forces everyone to be aware and deal with this deferred nonsense. And because they have to return it, they have to return a stupid microkit_notified_ret_nothing().

If you could OR all return values together then it would be okay. Then users can just return zero when not using it. For notifications that should work. But only for the first 63 signals. Of course we can just error out or send the signal immediately if it's > 63, that could be done in microkit_notified_ret_signal().

It wouldn't work for IRQs, but I don't see what the point of deferring IRQ ACKs is to be honest. Does anyone actually use microkit_deferred_irq_ack() and has it been tested to work?

Passing the return value as a pointer would technically work, too, it is what fault() does. It also relies on the single-notified-call property.

Yeah, except that it also uses the return value instead of only looking at reply_tag. But as there can only be one call or fault, using the return value isn't problematic.

I dislike passing return value as a pointer as (a) we have less than 64 bits of information necessary in the return anyway,

Only if you can OR all the return values together, otherwise you force the notified function to deal with all the details of deferred signals, because you lack the space to keep state.

and (b) it forces loads/stores from the stack,

Only if you actually do a deferred call. (And the compiler can optimise it away if it has global view.)
Sure, you need to check one stack value at the end to see if anything is pending, but that's cheap.

and there's no prevention against writing to it many times.

That's the main advantage.

If the type is opaque, the user can't write to it directly, but only via the deferred functions.

A user can always declare their own stack variable and return it later; they cannot declare their own return value instead of using the pointer argument.

You are missing the point, which is that if there is one shared data that keeps track of the state, the Microkit functions can automatically flush existing deferred signals when needed, instead of users open coding that themselves.

If there are multiple handler functions, you have to daisy-chain the return values and pass them as a parameter to each function and have a conditional deferred call based on its state in each handler function. And if anyone does this wrong, other code won't work correctly. Have fun debugging that!

I suppose you could ease the pain a bit by adding the last return value as a function argument for the defer functions, then at least the automatic flushing can be common code and users are more aware of the potential need of this.

All in all I propose keeping your return construction, but ORing the notifications together and getting rid of IRQ deferral. Then handlers can be independent and only the notified function needs to OR all return values together, which is easy enough to do. It makes the API nicely symmetrical too.

One issue with this proposal is that not splitting ny types in some way retains the existing property that channel IDs for notifications and PPCs are shared.

I don't think that's a problem. If users are aware of the 63 limit of notifications, then they will make all notifications IDs < 63.

In theory it is possible to not report conflicts if not necessary, e.g. [skip]

Yes, in practice you need to find the cap and you know whether you are dealing with a signal or notification, so it could be two separate namespaces.

Would not conflict at all. This seems... confusing.

A little bit yes. But it would work as expected, so why disallow it?

I'm not sure if my proposal actually improves on it much, but having the "type" of a channel just be an attribute on a particular ID implies that IDs are global across channel types.

I meant setting the attribute on the channel, to make clear that it only contains endpoints or notifications. E.g. type="ppc" would set notify=false for all end entries. But IDs in XML generally are globally unique, so it will always give that impression, except if you call them ppc_id and nf_id or something. But even then it implies it's global per type, while it is a namespace per PD.

To me it would make more sense to define all channels per PD instead of these loose channels that tie two PDs together and use two IDs from two different namespaces. Using your example, like:

<pd name="a">
  <channels>
    <end id="0" pd="b" notify=yes ppc=no />
    <end id="0" pd="c" notify=no ppc=yes />
  </channels>
</pd>

<pd name="b">
  <channels>
   <end id="0" pd="a" />
  </channels>
</pd>

<pd name="c">
  <channels>
   <end id="0" pd="a" />
  </channels>
</pd>

Because then all the IDs are together in the relevant location and from the same namespace.

Would not conflict or indeed

Missing sentence?

But I do like this, so I could integrate this into my split-per-type channel suggestion; since notably this doesn't work for ppcs, only notifications.

It could work for ppcs too, there can be multiple receivers for one endpoint. Useful for multithreaded servers or multiple servers for other reasons (like redundancy or lower latency).

Technically, no, this could be two separate changes. However, the existing API and the way notified works strongly implies the assumptions about channel IDs (global across channel types, 1:1 between sender & receiver, etc).

Yes, and I'm saying that that's fine because it simple. When people want to do more advanced stuff or run into limitations, then it's nice they can do that transitionally. Simple things stay simple, harder things are slightly harder to do, but still doable.

@Indanz

Indanz commented Aug 7, 2026

Copy link
Copy Markdown
Contributor

(I guess if you replace end with ppc and nft in my example, then you get explicit types too. Should make it easier for the tool to figure out whether to make and link endpoints and/or notifications.)

@midnightveil

Copy link
Copy Markdown
Author

It wouldn't work for IRQs, but I don't see what the point of deferring IRQ ACKs is to be honest. Does anyone actually use microkit_deferred_irq_ack() and has it been tested to work?

We do almost universally in sDDF use deferred_irq_ack.

@midnightveil

Copy link
Copy Markdown
Author

But having it as a return value forces everyone to be aware and deal with this deferred nonsense. And because they have to return it, they have to return a stupid microkit_notified_ret_nothing().

If they don't want to deal with deferred APIs, you only need to do that in notified(). I don't think that's too bad.

For any somewhat structured code, different notifications would be handled by calling different functions, and those are the ones that sometimes may want to do a deferred signal. Those different functions shouldn't need to be aware of each other. Doing deferral via return values is very awkward to do then.

It's awkward because you can only do one deferred call at a time. The current API and anything that has global state has the same awkwardness, but it just makes it easier to pretend that it doesn't exist. Especially with the current situation with one notified() call per channel, I suspect our sDDF drivers currently can accidentally overwrite a deferred IRQ because it's hard to think about it.

A return value enforces the single-return requirement explicitly, and forces the choice to be explicit.

If you could OR all return values together then it would be okay. Then users can just return zero when not using it. For notifications that should work. But only for the first 63 signals. Of course we can just error out or send the signal immediately if it's > 63, that could be done in microkit_notified_ret_signal().

I don't want to introduce an API that won't work if you exceed 63 channels for sending.

Besides, OR implies that you can do a batch deferred ack, in reality you can only do one? So Microkit would need to loop over it and perform each signal individually... unless there's plans to change the kernel to allow you to signal many notifications at once, in which case maybe that makes sense. (But we could also do this with microkit_notified_ret, it is, after all, a helper to construct a tagged union).

@midnightveil

Copy link
Copy Markdown
Author

Yes, and I'm saying that that's fine because it simple. When people want to do more advanced stuff or run into limitations, then it's nice they can do that transitionally. Simple things stay simple, harder things are slightly harder to do, but still doable.

Yeah. That was my intention with my proposal - with id simple and recv_id/send_id.

I'm not too fussed on the exact syntax in the SDF file. It's probably one of less happy things about this proposal in my mind, what to call this and how to describe it in the SDF.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants