Can't get sender from l4_ipc_wait()

Mai, Haohui haohui.mai at
Fri Apr 6 00:35:13 CEST 2012


It seems that l4_ipc_wait() will always set the sender to zero. I tested it
in example at /pkg/examples/sys/ipc/ipc_example.c, in the l4re-2011081207

Here is the patch I applied to the file (to print out label):

--- a/ipc_example.c     2011-08-12 00:20:36.000000000 -0500
+++ b/ipc_example.c       2012-04-05 17:29:24.844608359 -0500
@@ -84,6 +84,7 @@

+      printf ("IPC from %lx, %d\n", label, label == 0);
       /* So, the IPC was ok, now take the value out of message register 0
        * of the UTCB and store the square of it back to it. */
       l4_utcb_mr()->mr[0] = l4_utcb_mr()->mr[0] * l4_utcb_mr()->mr[0];

And here is the result I got:

vandroid| Sending:  4
vandroid| IPC from 0, 1
vandroid| Received: 16

So it seems that l4_ipc_wait() doesn't return the sender.

I'm writing an OS on top of Fiasco.OC. This information is important for
pager because it'll need it to figure out which page it'll map in.

Do you have any ideas to fix it, or any idea to work around it (at least
L4Linux works)? Your comments are appreciated.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the l4-hackers mailing list