seL4 / seL4_libs

No-assurance libraries for rapid-prototyping of seL4 apps.
https://docs.sel4.systems
Other
52 stars 62 forks source link

libsel4utils vspace implementation can only use vspace_new_pages for memory allocation #53

Open kent-mcleod opened 2 years ago

kent-mcleod commented 2 years ago

(Moved from https://sel4.atlassian.net/browse/SELFOUR-2429) A vspace_t manages memory allocations for a virtual address space and also handles mapping frames into these allocations.

libsel4utils provides a vspace implementation that can be bootstrapped within an existing address space (self-hosted) or alternatively manage a different vspace (as a loader). In both cases it must perform internal book keeping. In the self-hosted case there is a circular dependency for memory allocation that may need to extend the virtual address space. To handle this the implementation performs it's own memory management, IE it will allocate new book keeping memory by mapping some new pages in itself.

The issue is that it also tries to do this when allocating book-keeping data for a different vspace. Therefore in order to create a vspace for a different address space you must have an existing vspace for your current address space just to perform memory allocation for book keeping data. It would be great to be able to create a vspace that just uses malloc or an alternative memory allocator for its book keeping data.