On Sat, Dec 15, 2018, 3:19 PM Dave Richards <dave@synergy.org wrote:
Is it (or would it be) possible to specify more than the single root server module and have seL4 create virtual addresses, cap. Spaces, threads (leaving them suspended) and pass the information about these modules to the root server? In this way it would be possible to have GRUB load a multi-server seL4 environment
For UX/RT <https://gitlab.com/uxrt/>, the seL4-based OS I'm writing, I've added support for extra modules besides the root server, but all it does is make the Multiboot2 info structure and modules available to the root server. The root server is expected to load any further executables. Also, it currently requires the kernel and all modules to be embedded within a single filesystem image (using a special chain-loader) rather than loaded from separate disk files. UX/RT uses a process-per-subsystem-instance architecture rather than process-per-component, and its root server will contain everything needed to load normal user programs, so it will have no need for preloading executables besides itself. I did include support for preloading executables in my chain-loader (so the ELF loading code could be removed from the kernel), and it would be easy enough to remove the check that only one module has been preloaded, and it would also be relatively easy to change it to pass through modules that have been loaded from separate disk files, but having the kernel actually set up all the state for them would be a lot more difficult. It would be easier to just have the root server set up the state for the other executables if you want to split the core user-level components of your OS across multiple processes, but I'd say it would probably be a better idea to just do what I'm doing and put everything required to load regular processes in the root server. I really don't get why most microkernel OSes use process-per-component architectures. Security domains more often correspond to subsystems than components, and splitting subsystems into multiple processes usually just adds IPC overhead with little benefit for security or reliability.