GUEST_ASSERT(delta_ns * 100 < (t2 - t1) * 100);
 }
 
+static inline u64 get_tscpage_ts(struct ms_hyperv_tsc_page *tsc_page)
+{
+       return mul_u64_u64_shr64(rdtsc(), tsc_page->tsc_scale) + tsc_page->tsc_offset;
+}
+
 static inline void check_tsc_msr_tsc_page(struct ms_hyperv_tsc_page *tsc_page)
 {
        u64 r1, r2, t1, t2;
 
        /* Compare TSC page clocksource with HV_X64_MSR_TIME_REF_COUNT */
-       t1 = mul_u64_u64_shr64(rdtsc(), tsc_page->tsc_scale) + tsc_page->tsc_offset;
+       t1 = get_tscpage_ts(tsc_page);
        r1 = rdmsr(HV_X64_MSR_TIME_REF_COUNT);
 
        /* 10 ms tolerance */
        GUEST_ASSERT(r1 >= t1 && r1 - t1 < 100000);
        nop_loop();
 
-       t2 = mul_u64_u64_shr64(rdtsc(), tsc_page->tsc_scale) + tsc_page->tsc_offset;
+       t2 = get_tscpage_ts(tsc_page);
        r2 = rdmsr(HV_X64_MSR_TIME_REF_COUNT);
        GUEST_ASSERT(r2 >= t1 && r2 - t2 < 100000);
 }
 
        tsc_offset = tsc_page->tsc_offset;
        /* Call KVM_SET_CLOCK from userspace, check that TSC page was updated */
+
        GUEST_SYNC(7);
+       /* Sanity check TSC page timestamp, it should be close to 0 */
+       GUEST_ASSERT(get_tscpage_ts(tsc_page) < 100000);
+
        GUEST_ASSERT(tsc_page->tsc_offset != tsc_offset);
 
        nop_loop();