I'm not sure whether it's really "IPI" instead of "IPC", but it makes much more sense! There are also much better hits under Google for "IPI interrupt" than for "IPC" Interrupt. Additionally, "IPC" stands for Interprocess Communication, not for Interprocess Interrupt, as far as I know.