Hi, This addresses the review in two patches previously that could not be merged as is. Again, this allows SMP on 64 bit to boot.
TESTED: - Passes all i386 CI - Passes all x86_64 CI (except user32) - Boots to debian login with -smp 6 on a ncpus=8 x86_64 kernel Thanks, Damien
