/* should this be per processor send/receive? */
seq_printf(p, "IPI (recv/sent): %10u/%u\n",
atomic_read(&ipi_recv), atomic_read(&ipi_sent));
/* should this be per processor send/receive? */
seq_printf(p, "IPI (recv/sent): %10u/%u\n",
atomic_read(&ipi_recv), atomic_read(&ipi_sent));