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!!

Yuxin