Same file, except for whitespace, comment formatting and the
usage of wbinvd() instead of asm volatile("wbinvd":::"memory"), which is
the same.
Signed-off-by: Thomas Gleixner <tglx@linutronix.de>