Re: [seL4] Request for enhancement: Notification queues

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]

On 21 Jan 2020, at 14:29, Demi M. Obenour wrote:

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