I'd say scrap (a) _unless_ we're going to add while (1) loops to all the architectures. Alternatively, we could just accept that machine_power_off() may return and deal with that case (iow, not crash) in generic code.
What would the right behaviour be
while(1);
isn't really nice behaviour on a modern device