From 8e2df81ba88019aed7c94eea2f25e7822c989a3f Mon Sep 17 00:00:00 2001 From: Ivan-Velickovic Date: Wed, 13 Nov 2024 11:26:09 +1100 Subject: [PATCH] Do not resume TCB explicitly when advancing vCPU See comment for explanation, but essentially it's not necessary. Signed-off-by: Ivan-Velickovic --- src/arch/aarch64/fault.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/arch/aarch64/fault.c b/src/arch/aarch64/fault.c index efd5df43..1cca4dad 100644 --- a/src/arch/aarch64/fault.c +++ b/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);