I am currently using a Raspberry Pi 3b USB network card to run it based on sel4. I have encountered a problem where I need to use the hardware address of the USB register, which is 0x3f980000. Now I need to map this address to a virtual address in user space. I used the following method: i am currently using CAMKES to build a system to achieve my goals
connection seL4HardwareMMIO timer_mem(from rpi_driver.reg, to usbbase.reg);
connection seL4RPCCall hello_timer(from client.hello, to rpi_driver.hello);
}
configuration {
usbbase.reg_paddr = 0x3f980000; // paddr of mmio registers
usbbase.reg_size = 0x1000; // size of mmio registers
rpi_driver.sem_value = 0;
}
}
I am not sure if this method is correct. After mapping the register address to a virtual address using this method, will the properties of this virtual address be uncacheable and unbufferable? Because I have a hardware address, I must set the mapped memory properties to non cacheable and non cacheable. I don’t know how to use the CAMKES method to set the mapped memory properties.
The second issue is that I plan to try another method, without using the CAMKES framework, to directly call the sel4 API. I found some functions for address mapping, such as sel4_ ARM_ Page_ Map and seL4_ ARM_ Page_ MapIO, but I don’t know how to use these functions. I learned address mapping in the following sel4 tutorial: Mapping | seL4 docs
But the method provided in this tutorial did not set a specific physical address,He simply maps a physical page to a virtual address. For example, if I have a specific physical address 0x3f980000 now,size is 0x10000, how should I call these functions for address mapping,Map the physical register address to Virtual memory?Can you provide an example for me.
Thank you very much. Wishing you a pleasant life and smooth work. Looking forward to your reply.
Yes, the seL4HardwareMMIO connector creates mappings that are un-cached and writes won’t buffer. (I believe it uses the strongly ordered ARMv7 memory type).
You can look in the build directory for a *.cdl file. It’s a plaintext file that contains all of the frame objects and their mappings. If you search for 0x3f980000 in that file you should be able to check that the camkes configuration is at least selecting the right frame object and find where it is being mapped in the component’s virtual address space.
The physical address is encoded in the frame capability used to create the mapping. Working backward, the frame cap will refer to a frame that has been retyped from an Untyped cap. Untyped caps don’t virtualize memory and each one refers to a distinct range of physical addresses.
When the kernel launches the initial task, it gives an initial set of untypeds. The seL4_BootInfo_t structure has a section that describes each untyped cap in the initial set. In this description is the physical address and size of the untyped.
To create a physical address mapping at 0x3f980000 you would need to first create the frame cap from the untyped that covers the memory region that 0x3f980000 belongs to and then map that frame using sel4_ARM_Page_Map. It can be easy to get this allocation logic wrong, so there’s also another invocation, seL4_ARM_Page_GetAddress, which will return the base physical address of a frame cap.