The 128-bit multiply in pvclock.h was missing an output constraint for 
EDX which caused a register corruption to appear.  Thanks to Ulrich for 
diagnosing the EDX corruption and Avi for providing this fix (which now 
I am sending back to you Avi..)

Zach