Re: [seL4] Request for enhancement: Notification queues

Hi Gernot, Thanks for your prompt response! I was not expecting to get a response at all, much less such a fast one, so thank you. It is indeed straightforward to implement this in user-space. However, I have not found a way to do so that is both clean and performant. The naive approach requires one task for each notification to be polled on, which obviously is both slow and wasteful. There are faster approaches that use a user-space daemon. However, that still requires several context switches, as well as substantial complexity. It also requires all messages to go through a central broker, which is ugly, slow, and does not compose well with other seL4 features. The message broker would likely find itself becoming a buggy and slow reimplementation of much of seL4 itself. In my opinion, the main justification for putting this in the kernel is performance. seL4’s motto is “Security is no excuse for poor performance!”, and I believe that the performance improvement justifies the extra complexity in this case. seL4 makes the same decision in other places, such as IPC fast paths, so there is precedent. While a userspace implementation is possible, it will be substantially slower than a kernel implementation. I suspect that the performance overhead will be at least a factor of 2, due to the doubling of context switches. I consider this overhead unacceptable for an interface that will often be used in hot paths. I suspect the main reason that this has not been needed as much in the past is that static systems are less likely to need to wait on one of thousands of events to happen. However, as seL4 starts being used in highly dynamic systems, I suspect that this will become more and more necessary. I consider performance to be part of seL4’s required functionality, and my understanding is that the seL4 developers agree with this. While seL4 is currently mostly used in static systems via CAmkES, I believe that it has potential to be used in highly dynamic systems as well. It should be possible to build a full desktop OS on seL4, and for it to be just as fast as Linux. I hope to see one someday. Sincerely, Demi On 2020-01-20 23:04, Heiser, Gernot (Data61, Kensington NSW) wrote:

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

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel