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, <[email protected]> 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 [email protected]https://sel4.systems/lists/listinfo/devel
>
>
>
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to