seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
70 stars 37 forks source link

Have a "setvar" to reference Size of Memory Region from System Description in User Code #99

Open Bill-James-Ellis opened 5 months ago

Bill-James-Ellis commented 5 months ago

Hi, Microkit system description (XML) provides the map element, to map a memory region into protection domains. It has some attributes, including "setvar_vaddr", which specifies a symbol name in the program image (of type uintptr_t), which is rewritten to hold the start of the virtual address of the memory region. It's a nice means to declare constant decisions once in the high level system description, and make them available in the code.

An information gap we have with this, is that we sometimes need both the start of the virtual address for the memory region, and the size of that region. At the moment, we work around this, by assuming blocks are allocated contiguously, and deriving size from the gap between two addresses.

Instinctively, an additional map attribute might be apt to communicate size as well as the virtual address. But, I wonder if "size" is neither virtual nor physical specific, and would be the same value, and handy to know, in both contexts?

So, perhaps, maybe "memory_region" could provide a "setvar_size", to allow us to gain access to the size information? For example, something like: memory_region name="shared_heap" size="0x200_000" setvar_size="shared_heap_size"/>