Hi Peng, I do not fully understand all your questions, so will provide some generic responses. Our example ARM VMM runs on two platforms, which have different kinds of support for DMA. On the odroid-xu the VMM sets up the guest such that it has a 1-to-1 mapping, that is the IPA mappings are setup deliberately such that IPA is the same as PA. On the TK1 we support the system MMUs and the VMM asks seL4 to map frames into the same location in both the guest and systemMMU address spaces, resulting in an equivalent IPA->PA translation. In the case of doing DMA from a native seL4 thread it is your responsibility to know the physical address of memory that you use, or correctly setup the systemMMU. Adrian On Thu 05-Jan-2017 7:01 AM, PX wrote: Hi, all Happy new year! I have some urgent questions about address translation for a DMA driver in the ARM seL4-based VM. Your quick response is highly appreciated! 1. In the ARM sel4-based VM, the MMIO of a device is directly exposed to the device driver in the VM. When the DMA device driver allocates a DMA buffer to a device controller, the device driver can directly tell the real controller the IPA of the buffer starting address, instead of the real physical address. In other words, the device controller can only get the IPA of the buffer starting address. How can this device controller perform DMA without knowing the real PA of the buffer? Does seL4 perform some emulation here? How? 2. A closely related question to 1: when we develop a DMA driver in the VMM space, we put the real physical address of the device descriptor and real physical address of the DMA buffer in the controller registers through its MMIO. We found that the controller cannot find the correct place for the descriptor and the buffer. Do the seL4 hypervisor perform the address translation? If so, which source code does that? Thanks Peng _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel