-----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.cata...@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 -----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----- _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
