Skip to content

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

@kent-mcleod

Description

@kent-mcleod

(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.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions