# CONFIG_NO_HZ_FULL_ALL is not set