vmi_sched_clock   934 arch/x86/kernel/vmi_32.c 		pv_time_ops.sched_clock = vmi_sched_clock;
vmi_sched_clock    52 include/asm-x86/vmi_time.h extern unsigned long long vmi_sched_clock(void);