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, 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 listDevel@sel4.systemshttps://sel4.systems/lists/listinfo/devel

thanks, Adrian... Peng On Tue, Oct 4, 2016 at 9:05 PM, wrote:

The default configuration for the TK1 is to lazily map in devices as the VMM detects faults. This setting can be seen by make menuconfig -> Libraries -> VMM Library for ARM -> Allow on demand installation This will cause the VMM to interpret any fault from Linux as an attempted device access and attempt to map in said device. The important thing there is 'attempt' as the VM can still only map in devices that it itself has been given capabilities to. You can find this list by opening apps/vm/vm.camkes and finding the assignment to vm.mmios

Adrian

On Wed 05-Oct-2016 4:25 AM, PX wrote:

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, 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 listDevel@sel4.systemshttps://sel4.systems/lists/listinfo/devel