-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512
On Mon, Sep 26, 2022 at 01:00:03AM +0000, Gernot Heiser wrote:
On 23 Sep 2022, at 23:01, simone cataldo simone.cataldo@hotmail.it wrote:
Good morning,
We are a small test team, investigating seL4 microkernel to evaluate its use it as core component for a novel “open avionics” drone concept.
Essentially, we are starting from scratch, basing ourselves on the provided tutorials such as “hello world”. We were trying to modify its source code for evaluating basic thing simple functions, basic programs and custom libraries. However, it looks like the memory allocation is static and embedded in the original project: once we increase the complexity of the program it evidently causes trouble. We have not found any documentation about how to set the memory allocation at compile time, and how to include external dependencies (i.e. static libraries). We would like to have some guideline to get us started and direction to some in-depth documentation to acquire enough knowledge to build a full project of our own.
Hi Simone,
In terms of memory management, you need to distinguish the seL4 kernel from the rest of the seL4 system.
The kernel supports fully dynamic, policy-free memory management, my Advanced Operating System lectures describe how it works, see https://www.cse.unsw.edu.au/~cs9242/22/lectures.shtml
The recommended user-level framework CAmkES is, however, completely static.
The newer seL4 Core Platform has some dynamic functionality prototyped, but that does not yet expand to memory management.
However, we find that for most embedded/cyperphysical systems there is not much more need for dynamism than what is on the seL4CP roadmap (see https://trustworthy.systems/projects/TS/sel4cp/). There’s good reason for that: you don’t want your drone OS to fail in mid-flight because it’s out of memory. Typically, fully dynamic features are only needed for legacy support, which is catered for by virtual machines.
Gernot
Would it be possible/practical to allow seL4CP to have one or more PD that can run a full seL4-based OS? I am basically thinking of seL4-based containers here. - -- Sincerely, Demi Marie Obenour (she/her/hers) Invisible Things Lab