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 <[email protected]> on behalf of Andrew Warkentin 
<[email protected]>
Sent: Sunday, 16 December 2018 3:16 PM
To: [email protected]
Subject: Re: [seL4] Multiboot and extra modules

On 12/15/18, Dave Richards <[email protected]> wrote:
> 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
[email protected]
https://sel4.systems/lists/listinfo/devel

_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to