thanks, Adrian... Peng
On Tue, Oct 4, 2016 at 9:05 PM, <[email protected]> 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, <[email protected]> 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 [email protected]https://sel4.systems/lists/listinfo/devel >> >>
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
