double rounding in x86

[Tom Lynch]

Fred Tydeman has posted an interesting question on
comp.arch.arith about a double rounding case in the
x86 architecture:

1. A number which would be denormal in double precision is
   actually normal in the x86 fpu because of the extended
   exponent range.

2. A result, which in its exact form, is slightly less than
   the half way rounding point for the corresponding denormal
   form, is rounded to exactly this half way rounding point.
  
3. The value is stored to memory. This causes the exponent
   range to be reduced by making the significand denormalized, 
   and the extra precision is lost in a second rounding.
   This rounding may cause the number to be rounded
   up; hence producing a result different than that which 
   would have been produced under one direct rounding to the
   destination format.

IEEE std. 754 compatible?
other x86 idiosyncrasies?

Thanks,

Tom.Lynchaamd.com