Do not resume TCB explicitly when advancing vCPU

See comment for explanation, but essentially it's not necessary.

Signed-off-by: Ivan-Velickovic <[email protected]>

src/arch/aarch64/fault.c

@@ -27,7 +27,11 @@ bool fault_advance_vcpu(size_t vcpu_id, seL4_UserContext *regs)
     // For now we just ignore it and continue
     // Assume 32-bit instruction
     regs->pc += 4;
-    int err = seL4_TCB_WriteRegisters(BASE_VM_TCB_CAP + vcpu_id, true, 0, SEL4_USER_CONTEXT_SIZE, regs);
+    /*
+     * Do not explicitly resume the TCB because we will eventually reply to the
+     * fault which will result in the TCB being restarted.
+     */
+    int err = seL4_TCB_WriteRegisters(BASE_VM_TCB_CAP + vcpu_id, false, 0, SEL4_USER_CONTEXT_SIZE, regs);
     assert(err == seL4_NoError);
 
     return (err == seL4_NoError);