Hi Demi,
Thanks for your suggestion. The issue of some select-kind of feature keeps coming up.
In terms of the minimality principle [1], the question must be asked why this feature must be in the kernel. It seems to me that it would be straightforward to implement it on top of present seL4. What functionality are you after that is not possible to achieve with a user-level implementation, and what convincing use cases do you have for such functionality?
Furthermore, there is already a (restricted) form of similar functionality available. Instead waiting for a set of notifications, you can wait on a single notifications where different notifiers have different badges on their caps, and the badges have different bits set, so they can be distinguished even when multiple ones are signalled.
This latter version is restricted because of the limited size of badges (word size minus a few bits). I was thinking a while back whether we’d need a more general notion of notifications (that scale more) but have not yet seen a convincing use case.
Gernot
[1] Minimality principle: "A concept is tolerated inside the microkernel only if moving it outside the kernel, i.e., permitting competing implementations, would prevent the implementation of the system's required functionality.” [Liedtke, SOSP’95]
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
polled.
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.
Sincerely,
Demi