* executing with Secure TSC enabled, so special handling is required for
  * accesses of MSR_IA32_TSC and MSR_AMD64_GUEST_TSC_FREQ.
  */
-static enum es_result __vc_handle_secure_tsc_msrs(struct pt_regs *regs, bool write)
+static enum es_result __vc_handle_secure_tsc_msrs(struct es_em_ctxt *ctxt, bool write)
 {
+       struct pt_regs *regs = ctxt->regs;
        u64 tsc;
 
        /*
-        * GUEST_TSC_FREQ should not be intercepted when Secure TSC is enabled.
-        * Terminate the SNP guest when the interception is enabled.
+        * Writing to MSR_IA32_TSC can cause subsequent reads of the TSC to
+        * return undefined values, and GUEST_TSC_FREQ is read-only. Generate
+        * a #GP on all writes.
         */
-       if (regs->cx == MSR_AMD64_GUEST_TSC_FREQ)
-               return ES_VMM_ERROR;
+       if (write) {
+               ctxt->fi.vector = X86_TRAP_GP;
+               ctxt->fi.error_code = 0;
+               return ES_EXCEPTION;
+       }
 
        /*
-        * Writes: Writing to MSR_IA32_TSC can cause subsequent reads of the TSC
-        *         to return undefined values, so ignore all writes.
-        *
-        * Reads: Reads of MSR_IA32_TSC should return the current TSC value, use
-        *        the value returned by rdtsc_ordered().
+        * GUEST_TSC_FREQ read should not be intercepted when Secure TSC is
+        * enabled. Terminate the guest if a read is attempted.
         */
-       if (write) {
-               WARN_ONCE(1, "TSC MSR writes are verboten!\n");
-               return ES_OK;
-       }
+       if (regs->cx == MSR_AMD64_GUEST_TSC_FREQ)
+               return ES_VMM_ERROR;
 
+       /* Reads of MSR_IA32_TSC should return the current TSC value. */
        tsc = rdtsc_ordered();
        regs->ax = lower_32_bits(tsc);
        regs->dx = upper_32_bits(tsc);
        case MSR_IA32_TSC:
        case MSR_AMD64_GUEST_TSC_FREQ:
                if (sev_status & MSR_AMD64_SNP_SECURE_TSC)
-                       return __vc_handle_secure_tsc_msrs(regs, write);
+                       return __vc_handle_secure_tsc_msrs(ctxt, write);
                break;
        default:
                break;