# CONFIG_HZ_1000 is not set