[seL4] question about adding device to ARM VM linux

Hi, all I have a question about adding a device to ARM VM linux. When a device is added to the vmlinux, two functions, map_device () and map_ram () are invoked. I don't understand the purpose of map_ram().

In map_device(), the capacity to the device is used to set up the mapping between a virtual address and the MMIO (of the device). Then, in the map_ram (), a capacity to the virtual address is allocated. I am confused because the virtual address is already mapped to the mmio of the device. why do we need to allocate a capacity for the virtual address? Should the capacity be the same as the one for the device?

Thanks Peng