seL4
Consider auto-allocation of virtual addresses of mappings
Right now all mappings of memory regions require a virtual address given by the user. Most of the time, especially in conjunction with setvar_vaddr, you as the user might not really care about the specific virtual address as long as it is valid.
I haven't thought about it too much but I don't see a reason to make it so that if the vaddr attribute is missing then Microkit auto-allocates a virtual address, since it knows about the program image and other mappings, it knows the whole layout of the address space and therefore can figure out a valid one.
When there are multiple parties managing virtual address space, it's good to have clear rules who uses which address range. In this case it's the linker and Microkit, but also possible (future) dynamic memory managers.
An alternative would be to let the linker choose the virtual address, but that's probably harder to implement.
