Sorry for being slow in replying.

If anything can be done at user level it should, this is a fundamental aspect of seL4, and the core enabler of both its high performance as well as verifiability. Any diversion from that principle needs a very convincing case to be made (with a realistic and clearly important use case).

Please note that our promise to the community is that any changes we make to the kernel will be verified, and they cannot go into mainline until the official verified platforms have been re-verified. This means that the more invasive the proposed change, the more costly, and the stronger the justification needed.

At the moment, large dynamic systems are (unfortunately) not a high priority for seL4. I hope this will change in the foreseeable future, but right now we’ve got too many things that are higher on the list of priorities.

Also, I’m not convinced that even if we agreed that we wanted such functionality, your proposal would be the right way to do it. As I explained, Notifications already provide the same kind of functionality you are after, but the limited width of badges restricts it to a moderate number of notifiers. (At present that limitation is essentially given by the word size of 32-bit systems, that should definitely be changed on 64-bit systems, but even then it’ll be around 64.)

I strongly suspect the more fundamental and general extension would be to remove the scalability limitation of Notifications, probably by generalising them to a hierarchy, i.e. you signal a sub-notification which then signals the higher-level notification. I’m not claiming having thought this through, though.

But everything needs a really convincing argument, that’s based on a functional limitation that prevents implementation of certain important classes of systems. If it’s only a performance argument, we’ll need to be convinced that it really is a performance bottleneck in realistic systems.

Gernot