#include <linux/kernel.h>

typedef int (*PMIPC_TIMER_RUNTIME)(void*);