# CONFIG_NO_HZ_IDLE is not set