1.1 --- a/xen/arch/x86/domain.c	Tue Jul 15 16:13:46 2008 +0100
     1.2 +++ b/xen/arch/x86/domain.c	Tue Jul 15 17:56:25 2008 +0100
     1.3 @@ -286,6 +286,10 @@ int vcpu_initialise(struct vcpu *v)
     1.4  
     1.5      v->arch.flags = TF_kernel_mode;
     1.6  
     1.7 +    /* Ensure that update_vcpu_system_time() fires at least once. */
     1.8 +    if ( !is_idle_domain(d) )
     1.9 +        vcpu_info(v, time).tsc_timestamp = ~0ull;
    1.10 +
    1.11  #if defined(__i386__)
    1.12      mapcache_vcpu_init(v);
    1.13  #endif
    1.14 @@ -812,14 +816,6 @@ map_vcpu_info(struct vcpu *v, unsigned l
    1.15      for ( i = 0; i < BITS_PER_GUEST_LONG(d); i++ )
    1.16          set_bit(i, &vcpu_info(v, evtchn_pending_sel));
    1.17  
    1.18 -    /*
    1.19 -     * Only bother to update time for the current vcpu.  If we're
    1.20 -     * operating on another vcpu, then it had better not be running at
    1.21 -     * the time.
    1.22 -     */
    1.23 -    if ( v == current )
    1.24 -         update_vcpu_system_time(v);
    1.25 -
    1.26      return 0;
    1.27  }
    1.28