On Sat, May 25, 2024 at 07:40:39PM -0600, Andrew Warkentin wrote: > > I think the question you should be asking is what your goal is -- are > > you using seL4 because you specifically want to leverage seL4's > > properties? If so, launching off in another direction seems like the > > wrong move. If not, there are other L4-style microkernels you can use > > that don't have as many restrictions as seL4, and there's a largish > > community of advocates that will each be eager to help you decide to > > use theirs. > > AFAIK the only other active L4-like kernels are NOVA and Fiasco.OC,
Barrelfish? Also, compared to the cost of the rest of the system, dusting off a microkernel that's been on the shelf a bit is cheap. But IDK, I don't follow these in any detail. > My OS is going to be multi-server, although it will mostly have a > process-per-subsystem architecture like QNX does, and not a > process-per-component architecture like Genode or L4Re. Protection > domains correspond to subsystems more often than they do to > components, so there's not much point in splitting up components in a > lot of cases. Well, that depends. The whole premise of a microkernel is that you gain something by being in a separate address space and that it makes sense to split up the (traditionally unitary) kernel protection domain to gain that something. How finely you split it seems like a matter of taste. (Or, sometimes, religious doctrine...) > > The primary reason the world's gradually moved from that model of > > threads to a model where threads are second-class within processes > > is... design stupidity in pthreads. If you want to support pthreads, > > especially if you have any concerns about it being fast, don't go in > > this direction. > > I don't think I've seen any Unix-like OS that uses the thread model > I'm planning to use. They pretty much all either use a Plan > 9/Linux-like rfork()/clone() "threads are processes sharing state" > model, or a Mach-like "processes consist of state and threads" model, > rather than a "state is independent of processes and explicitly bound > to specific threads" model. The model I'm planning to use is a close > match to that of seL4, where capability spaces and virtual address > spaces exist independently of each other and threads. I don't see the difference between what you're describing and the rfork/clone model. But in any event, the problems with pthreads remain; it's difficult to implement the pthreads behavior of fork/exec/wait in a model where threads aren't tied to processes. > > > Another thing that I'm not sure about is the real-time performance. In > > > addition to desktop and server use, embedded systems with hard > > > real-time constraints are also an important use case for this system. > > > > In that case you want to stay a long way away from anything that looks > > like Unix. > > QNX is Unix-like and has reasonable performance for real-time systems, > although of course it is quite different from conventional Unix in its > architecture. It only looks like Unix from the outside, and not all that much even then... -- David A. Holland dholl...@netbsd.org