On 12/15/18, Dave Richards
I have not read the ukernel code, but I would imagine that most of the code needed to launch the multiple servers already exists, i.e. it is necessary to launch the root server. It may require re-factoring, of course. Right?
It solves another immediate problem for me. I can develop the various servers without working on device drivers, I/O subsystem, ELF loader, etc.
Yes, there's code to launch the root server, but it's not particularly general, and is just enough to set up the state for the root server's initial thread. It would probably be non-trivial to make it general enough to load multiple servers. Personally I don't think that the kernel should be setting up state for multiple servers though. I'd say that it should leave it up to the root server (my chain-loader's ELF preloading code would make that relatively easy to do from a root server without an ELF loader built in. although UX/RT's root server will just use its own built-in loader since it will treat modules as files rather than processes, and will only start /sbin/init directly, with init starting all other processes; I think a microkernel OS should have as few "special" servers as possible).
As for the OS architecture, I imagine many approaches are possible depending on the goals of the designer. The nice thing about seL4 is that it doesn't dictate any single approach.
What kind of OS are you trying to write? UX/RT is going to be a QNX-like OS with some concepts from Plan 9 thrown in, as well as a high degree of Linux compatibility.