RT_PUSH_IPI        77 kernel/sched/features.h SCHED_FEAT(RT_PUSH_IPI, true)
RT_PUSH_IPI      2072 kernel/sched/rt.c 	if (sched_feat(RT_PUSH_IPI)) {