Hi Peng,

I would prefer to say that the RAM used by the VM starts at physical address 0xb0000000, and is just one of many physical memory regions on the device. I'm not sure why you refer to a 'VM memory boundary' as no such thing exists, there are just many physical memory regions that are given to the VM, RAM merely being a fairly large one of these.

Everything that the VM touches is explicitly put into the stage 2 translation (ARM EPT equivalent). If you want to trace the installation of MMIO regions (as opposed to the RAM) then you can follow the implementation and usage of 'map_vm_device' from (libsel4arm-vmm/src/devices.c).

Adrian

On Tue 04-Oct-2016 7:07 AM, PX wrote:

Hi,
I have questions about the device drivers in the virtual machine on ARM seL4. The virtual machine on TK1 board is located on the physical memory starting at 0xb0000000. However, the MMIOs used by the device drivers in the VM are below 0xb0000000.

1.If my understanding is correct, does that mean that a device driver in the VM can actually access a memory block outside of the VM's boundary even though it is mmio.

2. If the device driver actually uses the mmio outside of the VM's memory boundary, do the page tables (including EPT) need to map to this mmio? However, I can not find any code doing the mapping.

Do I miss something?

Thanks

Peng
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel