On Sat, Dec 15, 2018, 3:19 PM Dave Richards 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.