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