On 2020-01-21 20:41, Heiser, Gernot (Data61, Kensington NSW) wrote: > On 21 Jan 2020, at 15:31, Demi M. Obenour <demioben...@gmail.com> wrote: >> >> 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. > > Sorry for being slow in replying.
Not a problem! > If anything can be done at user level it should, this is a fundamental aspect > of seL4, and the core enabler of both its high performance as well as > verifiability. Any diversion from that principle needs a very convincing case > to be made (with a realistic and clearly important use case). > > Please note that our promise to the community is that any changes we make to > the kernel will be verified, and they cannot go into mainline until the > official verified platforms have been re-verified. This means that the more > invasive the proposed change, the more costly, and the stronger the > justification needed. > > At the moment, large dynamic systems are (unfortunately) not a high priority > for seL4. I hope this will change in the foreseeable future, but right now > we’ve got too many things that are higher on the list of priorities. > > Also, I’m not convinced that even if we agreed that we wanted such > functionality, your proposal would be the right way to do it. As I explained, > Notifications already provide the same kind of functionality you are after, > but the limited width of badges restricts it to a moderate number of > notifiers. (At present that limitation is essentially given by the word size > of 32-bit systems, that should definitely be changed on 64-bit systems, but > even then it’ll be around 64.) > > 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. > > But everything needs a really convincing argument, that’s based on a > functional limitation that prevents implementation of certain important > classes of systems. If it’s only a performance argument, we’ll need to be > convinced that it really is a performance bottleneck in realistic systems. > > Gernot > > > _______________________________________________ > Devel mailing list > Devel@sel4.systems > https://sel4.systems/lists/listinfo/devel > On Tue, Jan 21, 2020, 8:42 PM Heiser, Gernot (Data61, Kensington NSW) <gernot.hei...@data61.csiro.au> wrote: > On 21 Jan 2020, at 15:31, Demi M. Obenour <demioben...@gmail.com> wrote: > > > 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. > > > Sorry for being slow in replying. > Not a problem. If anything can be done at user level it should, this is a fundamental > aspect of seL4, and the core enabler of both its high performance as well > as verifiability. Any diversion from that principle needs a very convincing > case to be made (with a realistic and clearly important use case). > Agreed. I consider scalable communication between userspace applications to be such a use case, but I understand if you do not. > Please note that our promise to the community is that any changes we make > to the kernel will be verified, and they cannot go into mainline until the > official verified platforms have been re-verified. This means that the more > invasive the proposed change, the more costly, and the stronger the > justification needed. I 100% agree. At the moment, large dynamic systems are (unfortunately) not a high > priority for seL4. I hope this will change in the foreseeable future, but > right now we’ve got too many things that are higher on the list of > priorities. Me too. I was attracted to seL4 mostly because of the hope that it could replace Xen in QubesOS. QubesOS certainly qualifies as a large dynamic system! > Also, I’m not convinced that even if we agreed that we wanted such > functionality, your proposal would be the right way to do it. Me neither! If it was, I would be highly surprised. The reason I proposed it is that it is the best one I could think of, and because it does not require userspace to keep side tables. > As I explained, Notifications already provide the same kind of > functionality you are after, but the limited width of badges restricts it > to a moderate number of notifiers. (At present that limitation is > essentially given by the word size of 32-bit systems, that should > definitely be changed on 64-bit systems, but even then it’ll be around 64.) The scalability problem is what worried me. It also seems to be a problem for others, who (unlike me) are actually building stuff based on seL4. > 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. That approach seems good. It does require side tables, but it is probably significantly less intrusive. Being able to read multiple levels of notifications in a single system call would be especially helpful. > But everything needs a really convincing argument, that’s based on a > functional limitation that prevents implementation of certain important > classes of systems. If it’s only a performance argument, we’ll need to be > convinced that it really is a performance bottleneck in realistic systems. Do you believe it is likely to be? Highly dynamic systems generally avoid arbitrary limits (not imposed by the physical hardware) whenever possible, since someone *will* eventually hit them. That said, one could make a decent argument that a typical userspace client process will not have over 20 processes that will be sending data to it at high speed. Most userspace processes don’t simultaneously interact with 20 different subsystems of a monolithic kernel, after all. I would expect a userspace process to need to receive notifications from network, graphics, input, storage, Bluetooth, and USB subsystems. Everything else will likely be low-speed control messages, which can be handled by a userspace bus. Implementing D-Bus on top of seL4 IPC would be a nice project. > Gernot Demi
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
