Hi all,
Just to confirm what has already been stated: while it would be possible for seL4 to load multiple images, however this is incongruent with L4 philosophy. We want to keep the kernel as small as possible to minimise the trusted computing base and maximise policy freedom.
The root task can act as a loader to load multiple images according to whatever policies suit the system. One example loader we have is the capdl loader (https://github.com/seL4/capdl) which can load capabilities and set up processes based on a specification.
Camkes (https://docs.sel4.systems/CAmkES/) can be used to initialise such specifications.
We're working on improving our documentation and tools for setting up seL4 systems, so keep an eye out in the coming year.
Cheers,
Anna.
________________________________________
From: Devel
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. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel