I'm trying to write a multithreaded seL4 application. It's to be made up of sel4util processes with different cspaces and sharing the same Vspace.

I managed to achieve this, but what confuses me is that since the processes share the same Vspace, wouldn't GetIPCBuffer() return the same result for each of them? I looked at libsel4/arch_include/arm/sel4/arch/functions.h, and GetIPCBuffer() is simply:

Since seL4_GlobalsFrame is just a fixed memory location (0xffffc000) in the shared address space, why does seL4_GetIPCBuffer() return different results for different processes? Below is the output:

Is it that the frame ffffc000 mapping is changed on every context switch perhaps? Can I absolutely trust that IPC is still working correctly with this set up?

Thanks,

David