Take it out of smpboot.c, and move it to process_32.c, closer
to its only user.
Signed-off-by: NGlauber Costa <gcosta@redhat.com>
Signed-off-by: NIngo Molnar <mingo@elte.hu>