= CPU 0 =                                            = CPU 1=

detach_and_destroy_domain {
            rcu_assign_pointer(cpu1_dom, NULL);
}

dom = new_domain(...) {
             nr_cpus_busy = 0;
             set_idle(CPU 1);
}
                                                    clear_idle(CPU 1)
                                                    dom = rcu_dereference(cpu1_dom)
                                                    //dom == NULL, return
rcu_assign_pointer(cpu1_dom, NULL);

                                                    set_idle(CPU 1)
                                                    dom = rcu_dereference(cpu1_dom)
                                                    //dec nr_cpus_busy, making it negative