Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

sel4vm: Remove vspace dependency #97

Open
kent-mcleod opened this issue Apr 25, 2023 · 0 comments
Open

sel4vm: Remove vspace dependency #97

kent-mcleod opened this issue Apr 25, 2023 · 0 comments

Comments

@kent-mcleod
Copy link
Member

This is a breaking change but is probably worthwhile to consider:

Removing the vspace_t dependency from libsel4vm and libsel4vmmplatsupport
and interacting with the vspace objects directly mostly resolves a series of issues
and don't really introduce any significant new problems for guests or a client vmm
other than needing to update vmm drivers that expect to use the vspace objects.
It also provides a reasonably small stepping stone for eventually removing more of
sel4_libs as discussed recently (https://sel4.discourse.group/t/sel4-virtualization-support-current-efforts/665/3)

vspace_t is an abstraction that wraps seL4 vspace objects and provides
the following functionality:

  1. Mapping intermediate page table objects automatically
  2. reserving regions for future mapping
  3. Helper functions for creating OS objects like ipc buffers and stacks
  4. Tracking reserved regions in the address space like kernel window
    mappings
  5. Unmapping vspace entries indexed by virtual address
  6. Creating shared mappings from one VSpace into another vspace indexed
    by virtual address
  7. Automatic placement of anonymous memory regions (eg mmap)
  8. Automatic allocation and mapping of any internal book-keeping data
  9. self-hosted or remote management of Vspaces where a vspace can refer
    to the current process address space or a different address space.
  10. A way to iteratively and dynamically map frames from another vspace
    into the callers vspace and call a callback function with the mapped
    window as an argument. The mapping is then removed when the callback
    returns.

Unfortunately there are the following issues:

  • The book-keeping data allocation can only happen through a vspace_t
    instance. For book-keeping a VM's vspace, the host must then also
    have a vspace_t for managing its own vspace, a host may not want this
    level of dynamism
  • The book-keeping data doesn't currently do anything clever for large
    frames and still keeps a unit of data for every 4k range of memory
    used in the vspace. So a 2MiB mapping would have 512 duplicate
    book-keeping entries, and a 1GiB would have 51251216bytes = 4MiB
    overhead.
  • Encouraging implementations to use the shared-memory iterator leads to
    very inefficient emulated drivers as mapping and unmapping are usually
    more expensive than short memcpys and dominate the operation time.

The VMM only really needs features 1, 2 and 9, and it already implements
its own version of region reservations (2) separately. There's also some
helper functions in libsel4utils that implement just 1. and depend on a
vka_t interface that the VMM also already has a copy of.

As for 6. the vmm does need a more efficient copyin/copyout mechanism
that would be somewhat system specific and shouldn't create new mappings
on each access.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant