Question about IPI

Yuxin Ren ryx at
Thu Jul 17 19:03:31 CEST 2014

Hi All,

Now I want to how many IPIs are sent during an IPC. So I add a counter for
IPI in the kernel, and in the user level, there is a client sending IPC to
a server on another core.
But I found some behavior are very strange.

1. The total number of IPI are not multiple times of the number of IPC. It
seems that there are some "extra IPIs", and with the number of IPC
increases, the number of "extra IPIs" are also increasing.
  So my question is if there are some background program in the kernel or
L4Re to send IPIs?

2. If I add printf statement in the kernel, the number of IPIs are also
increasing. Does printf in the kernel cause sending IPI? If it does, is
there any methods to avoid this. Like in Linux, it has printk function in
the kernel.

Thanks a lot!!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the l4-hackers mailing list