[seL4] Re: Support for Sel4 Project

-----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 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 -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEdodNnxM2uiJZBxxxsoi1X/+cIsEFAmMxAVQACgkQsoi1X/+c IsGJghAApAeYEdFv3GSWprU6J58cQtvdy+GSV3+j8hZt5/zVabPpSDupSpa0LGfN HFQe19PeltkCdXB16L1qdXSFi9GnuR4547pIoADzzFiBOwMosUGnMf47gkSYnkuH KcAAdXV2i8YEngWV2RBhgGnThxKiEx6NUf18y3Si3nngY/f85ZDg0bRGCRthEKKx 8Xv2oAnb2MQbtIadINvB8VDfebUcmFGCDJssfm0IRczzfSbSMNKmDIfvl4NoQcNL 8NfVOghzl2nTFJ+3fe4SPvOsbAjJLat23yhLIWFKZOvNM76yciazv+GMuIQFqqYx C9xvVIhRV3WjxzepuY4vc/jvWYD6J3smDEMj6IBN1bDzxIU3L88kjjaG9yqE3VbW R3vlJ/UbqgqBTqZKixA7uWubWWj2NrMm0JKVegmyQgqNEnU9QR3qhPeiECBY2qSI pPN2iqVO+wcMfpsOWxo6XGCYlO4za+i13JNkGPUKnUBCk9qCmsli13+Z5KjAOktk caNfGxVxRh1bzJ2VZdyhlgV8YuCbUXQcthKmwPs0vYT+yzjuMgGAfQLwA/S8n9g2 DXIGWQNy+t6nICgOXIyZ0eJ6rt62zQFnvgDXWnxYBTHYvwcajnUVE7Z5jDEB84Ii Q4uymQB6H6Ziwv3ljIFxZDOwfJUDDGl7CQOBgtULIQULADceABs= =0aAC -----END PGP SIGNATURE-----