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
Devel@sel4.systems
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
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel