Hi David, The global frame is a location of memory that is updated by the kernel whenever a thread switch happens. It acts as a form of thread local storage. See https://github.com/seL4/seL4/blob/51ef223945b06d38dbc9d3f6ffcee795966428d0/src/arch/arm/32/kernel/thread.c#L22
So yes, your IPC will work correctly and as intended. It would be strictly incorrect for different threads to try and use a single IPC buffer. Adrian On Wed 16-Mar-2016 6:47 PM, Qiwei Wen wrote: Hi, 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: return *(seL4_IPCBuffer**)seL4_GlobalsFrame; 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: ========================== PARENT: IPCBUFFER: 00273000 CHILD: GlobalsFrame: ffffc000, *GlobalsFrame 10076000 CHILD: setting shared to 97 PARENT: CHILD DIED, shared char: 97, MR16: 00000000 ============================= 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 _______________________________________________ Devel mailing list [email protected]<mailto:[email protected]> https://sel4.systems/lists/listinfo/devel ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
