272512 /* per-cpu version of normal_pdes */ /* Ok to hardcode. only for x86_64 && XEN */