[JoshTriplett]

Linux still needs to use a Startup IPI to bring up other CPUs, which starts them running in 16-bit mode at an address under 1MB.

Having a fully 64-bit way to bring up other CPUs would simplify that.