Adrian,

Thanks for your answers. However, I am confused with linux_pt_devices[]. The MMIO mapping is done through this data structure, each device in the list will be mapped into the page table in the VM. But this device list for tk1 linux virtual machine is empty! I guess this list will be populated by some code, but I cannot find the code that fill this list. How is this list filled? by whom?

thanks

Peng

On Mon, Oct 3, 2016 at 6:42 PM, <Adrian.Danis@data61.csiro.au> wrote:

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