Vmm Guest Memory Related Configure

seL4 kernel
1

Hi there:

While portinging Android Guest based on Sel4 Vmm project, I met some problems .In my porting steps, I increased the reserved memory for Android Guest to 2G on my platform. Then there were some parts of Sel4 Vmm project that confused me.

  1. the principle to determin the static pool size for bootstrap with allocman
     In bootstrap.h, I found your explanation for the value that it is based on the work with trial and error.Is that still the case?
     If I incease this size, the frame_vm0_group_bin showed in vm_minimal.cdl file will obviously increase together.What’s the relationship of the two value?

  2. How is the staic memory pool created?
    Is this memory pool created from untyped memory, so as treated untyped object?

  3. the principle to determin the vm.simple_untyped24_pool size and nums
     What’s the usage of the untyped_pool memory?
     How can I make sure a reasonable size and nums of this value ?

Much apprecitated, if you can give some feedbacks!

2

Hi,

  1. The static pool size looks to be set arbitrarily to 80MiB (camkes-vm/main.c at master · seL4/camkes-vm · GitHub) this is essentially the heap of the vmm component.
  2. This pool is created inside the .bss section of the binary and so memory will be allocated and initialized for it automatically.
  3. If you want a 2G memory for the guest, then you should declare this range using vm0.untyped_mmios in the CAmkES ADL file to refer to the reserved memory you made. untyped_pool memory is used for allocating objects that can be used by the VMM or the guest. It may require increasing to support the Page table objects required to set up a 2GiB mapping.
3

Hi,thanks for your answering. And for the 3rd question, I want to know how can I configured the reasonable value for the size and nums of this untyped_pool memory. Accordingly, to my analysis, this configuration may influence the allocating effeciency of objects that can be used by the VMM or the guest.