While studying seL4, I noticed that there is no mechanism to wait for
one of many notifications. This proposal solves this with a new type
of capability, which I call a notification queue.
I don’t have the knowledge to determine how they should be
implemented, so instead I will describe the general idea.
A notification queue is a capability to which notification
objects can be attached. When an attached endpoint is notified, a
user-provided pointer is pushed onto the queue. Notification queues
are edge-triggered, so subsequent notifications do not cause further
entries to be added to the queue unless the notification has been read.
The queue is implemented as a buffer which is read-only to userspace,
but read-write to seL4. When creating a notification queue, userspace
must provide sufficient untyped memory to ensure that the queue will
not fill up. This ensures that sending a notification cannot fail
due to resource exhaustion. Queues can be resized by the application
if needed. Attempts to add too many endpoints to a queue results in
an error being returned.
A notification object can only be attached to one notification queue at
a time. It can be detached from a queue and later attached to another.
Notification queues can be used whenever a notification object is
expected, except that they cannot be badged. Badging a notification
queue would make no sense. When polled, a notification queue returns
the number of events that have been added to it since it was last
Adding one notification queue to another may or may not be
allowed. Allowing it would increase flexibility, but also increase
implementation complexity. It is also possible to attach a TCB to
a queue; the queue is notified when the TCB exits.
Only seL4 can send to a notification queue. No userspace process
can ever possess a send capability to such a queue.
While a notification queue can be accessed from any number of tasks,
performance on multi-core systems may be improved if each queue is
used from the same core that its attached notifications are used on.
Constructive feedback on this proposal is welcome.