To add a bit to what Gernot said, it is technically possible to configure two threads to have the same IPC buffer.
However, the resulting system is not useful. The threads trample each other's system calls and IPC attempts. In the
worst cases, thread interleavings result in the equivalent of torn writes to your IPC buffer and your kernel invocations
start looking like random noise. We observed this early on in the development of CAmkES when we accidentally configured
systems this way. I would not recommend the experience.
On 20/03/16 13:36, Gernot Heiser wrote:
seL4 IPC is a bit different to SYS-V in very fundamental ways, so comparisons
may not be all that meaningful.
In particular, the seL4 IPC buffer is a set of *virtual registers*. This means
it has the semantics of physical
registers: they are strictly thread-local (which includes that any attempt by a
thread to access another thread’s IPC
buffer has undefined result) and cannot page fault. This is a fundamental
design decision, not policy.
Gernot
On 20 Mar 2016, at 12:48 , Tom Mitchell <[email protected]
<mailto:[email protected]>> wrote:
There are questions of policy.
Two processes or threads with the same security label could
share a buffer used for IPC.
A new buffer needs to be scrubbed of any data so no side channel or
data leak is generated by object reuse.
SystemV IPC could be sloppy with this and demand that the user
create the buffer with correct permissions. The simple owner, group, world
set of permission bits is not sufficient.
Failure to dismiss and delete the object was another SysV demand
made on the application programmer.
Threads must have ways to communicate...
Even sending signals that can be caught to a process or thread can qualify as
a data communication path to violate policy and generate side channels.
...___...
Interesting tip of the iceberg question.
On Thu, Mar 17, 2016 at 12:04 AM, Adrian Danis <[email protected]
<mailto:[email protected]>> wrote:
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] <mailto:[email protected]>
https://sel4.systems/lists/listinfo/devel
--
T o m M i t c h e l l
_______________________________________________
Devel mailing list
[email protected] <mailto:[email protected]>
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
