Re: [seL4] Request for enhancement: Notification queues
by Millar, Curtis (Data61, Kensington NSW)
> 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.
Having thought about this a little, I think that it is useful to observe
that the case where such cases where large numbers of notifications need
to be received the receiver uses a roughly similar interface to
endpoints (seL4_Send to wait for an event and seL4_NBSend to poll for
If we allow send queues of endpoints to include notification objects in
addition to threads we could multiplex notifications via an endpoint by
binding the notifications to the endpoint.
This could also allow for the removal of notification binding for
threads; if they want to receive both notifications and synchronous IPC
they can bind the notification to the endpoint. This design should also
work with MCS whereby donation of scheduling contexts from notification
objects would become roughly the same as donation from a thread with a
I think the cleanest implementation would be to allow a notification to
contain its own endpoint capability, similar to the manner in which TCBs
conatain capabilities. Any time an idle notification is invoked with a
send it then queues on the endpoint to which is capability refers if one
exists. Send invocations of 'active' (potentially queued) notifications
would perform the same XOR operation as currently occurs.
When receiving on an endpoint where the first blocked object is a
notification the badge received is the badge of the endpoint capability
owned by the notification and the notification word is simply placed in
the first message register.
Whilst I think that this (or something similar) is the most simple case
for implementing multiplexing it would have some impact on the semantics
and implementation of some objects. Even at this small a scale the
verification burden will still be considerable as this change would
impact all verified builds.
I think further discussion and evaluation of a solution is needed before
we can determine that it is sufficiently beneficial to have this feature
in the kernel and to commit to maintaining the feature and including it
in the verified configurations.