record_times      692 kernel/sched/psi.c 	record_times(groupc, cpu, false);
record_times      801 kernel/sched/psi.c 		record_times(groupc, cpu, true);