rcu_sched_clock_irq 77 include/linux/rcupdate.h void rcu_sched_clock_irq(int user); rcu_sched_clock_irq 1726 kernel/time/timer.c rcu_sched_clock_irq(user_tick);