portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

mcs: add check for preemption to SysReplyRecv

Browse source 
To ease verification, in the SysReplyRecv case of handleSyscall, add
the explicit check for preemption, even though the call to
handleInvocation should not be preemptible.

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney 2026-05-29 11:03:59 +09:30 committed by Gerwin Klein
parent 93f73a49ad
commit a15e9a32a2
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/api/syscall.c
View file

@ -596,8 +596,12 @@ exception_t handleSyscall(syscall_t syscall)
case SysReplyRecv: {
cptr_t reply = getRegister(NODE_STATE(ksCurThread), replyRegister);
ret = handleInvocation(false, false, true, true, reply);
/* reply cannot error and is not preemptible */
assert(ret == EXCEPTION_NONE);
/* reply is not preemptible, but to ease verification we check explicitly */
if (unlikely(ret != EXCEPTION_NONE)) {
mcsPreemptionPoint();
checkInterrupt(/* was_interrupt_entry */ false);
break;
}
handleRecv(true, true);
break;
}