Adrain,
You answer is exactly what I want to know. For the TK1 support, I guess I misunderstand the SMMU support code. From my understanding, the RAM of the VM on TK1 board consists of the physical memory block starting at 0xb0000000 and 1:1 mapping MMIO space.  Do I miss something here? where is the SMMU support code? which libraries should I check for the SMMU support?

thanks
Peng

On Wed, Jan 4, 2017 at 7:29 PM, <Adrian.Danis@data61.csiro.au> wrote:
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.systems
https://sel4.systems/lists/listinfo/devel