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

Hey Simone, I have been working on an seL4 project from relative scratch recently, and trying to build some degree of custom dynamic memory management. CAMkES and the seL4 CP are probably better established starting places for seL4 systems, but they were a bit too prescriptive for my particular (research) project, so I have been exploring and using the many more precise library tools available for working ontop of seL4. The following pointers from my experience may be helpful: The seL4 allocman library (libsel4allocman) can be used to manage most of the complex low-level seL4 allocation problems that have to be handled in most systems (Untyped memory splitting, CSpace slot management, and storing allocation bookkeeping memory in the same set of memory being allocated). An allocman instance can be bootstrapped from the bootinfo argument that the seL4 root task gets handed, which will make it pick up all the memory caps available in the system post-kernel-boot, as specified in the bootinfo. An allocman instance can also export a 'vka' interface (defined via libsel4vka), which allows for simple allocation requests for arbitrary seL4 kernel objects (vka_alloc_object()) such as threads, new cspaces/page tables, etc. A vspace (libsel4vspace) instance can be set up to more directly manage a virtual address space (i.e. page table), using a VKA instance (passed in in the vspace setup) for grabbing the required new kernel objects/capabilities (pages, page table mappings, backing physical memory etc) when required. You can see all of these facilities at play and the bootstrap/setup calls required in the 'roottask-test' project I've published here https://github.com/nuclearpidgeon/seL4-roottask-test/blob/main/roottask/main... , which I put together from pieces of seL4test, seL4bench, and the UNSW AOS boilerplate project. Once you have a vspace set up, vspace_new_pages() in libsel4vspace can be used as a rough equivalent to linux mmap(), to pull more pages into the current virtual address space. At the end of this journey of getting your hands on a vspace and its API, you can also start using the malloc() implementation provided in libsel4muslcsys. Take a look at https://github.com/seL4/seL4_libs/blob/master/libsel4muslcsys/src/sys_moreco... . If libsel4muslcsys has been compiled without a static heap (CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES = 0), it will try use a 'muslc_this_vspace' variable (that it expects to be set by system/process setup) and appropriate vspace API calls (such as vspace_new_pages()) to actually handle malloc() requests by backing them with mapped virtual memory. Cheers (and good luck...), Stewart Webb (Computer Science Masters student at the University of Melbourne)