diff --git a/driver/gator_iks.c b/driver/gator_iks.c
index 24233d775581b284fa76644d93f8bf35ff7f5eb0..0a90bdd1904e95bde89cd08466ad506573971e21 100644 (file)
--- a/driver/gator_iks.c
+++ b/driver/gator_iks.c
{
int cpu;
// Send the cpu names
+ preempt_disable();
for (cpu = 0; cpu < nr_cpu_ids; ++cpu) {
if (mpidr_cpus[cpu] != NULL) {
gator_send_core_name(cpu, mpidr_cpus[cpu]->cpuid, mpidr_cpus[cpu]);
}
}
+ preempt_enable();
}
static int gator_migrate_start(void)