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