CPU_MONDO_COUNTER
xc_rcvd = CPU_MONDO_COUNTER(first_cpu);
target_cpu_busy = (xc_rcvd < CPU_MONDO_COUNTER(first_cpu));