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

mcs: refactor reply functions to ease verification

Browse source 
The outermost if statement can be removed in reply_pop
because reply_pop is called only in reply_remove, which
includes an explicit check for this condition.

The new inline function setThreadStateBlockedOnReply is
used within reply_push.

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney 2025-03-31 13:51:35 +10:30 committed by Gerwin Klein
parent 58f0e87355
commit fd14374e9d
2 changed files with 23 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
include/kernel/thread.h
View file

@ -307,5 +307,12 @@ void awaken(void);
/* Place the thread bound to this scheduling context in the release queue
* of periodic threads waiting for budget recharge */
void postpone(sched_context_t *sc);
static inline void setThreadStateBlockedOnReply(tcb_t *tptr, reply_t *reply)
{
thread_state_ptr_set_tsType(&tptr->tcbState, ThreadState_BlockedOnReply);
thread_state_ptr_set_replyObject(&tptr->tcbState, REPLY_REF(reply));
scheduleTCB(tptr);
}
#endif

36
src/object/reply.c
View file

@ -30,8 +30,7 @@ void reply_push(tcb_t *tcb_caller, tcb_t *tcb_callee, reply_t *reply, bool_t can
/* link caller and reply */
reply->replyTCB = tcb_caller;
thread_state_ptr_set_replyObject(&tcb_caller->tcbState, REPLY_REF(reply));
setThreadState(tcb_caller, ThreadState_BlockedOnReply);
setThreadStateBlockedOnReply(tcb_caller, reply);
if (sc_donated != NULL && tcb_callee->tcbSchedContext == NULL && canDonate) {
reply_t *old_caller = sc_donated->scReply;
@ -41,12 +40,12 @@ void reply_push(tcb_t *tcb_caller, tcb_t *tcb_callee, reply_t *reply, bool_t can
SC_PTR(call_stack_get_callStackPtr(old_caller->replyNext)) == sc_donated);
/* push on to stack */
reply->replyPrev = call_stack_new(REPLY_REF(old_caller), false);
if (old_caller) {
old_caller->replyNext = call_stack_new(REPLY_REF(reply), false);
}
reply->replyNext = call_stack_new(SC_REF(sc_donated), true);
reply->replyPrev = call_stack_new(REPLY_REF(old_caller), false);
sc_donated->scReply = reply;
reply->replyNext = call_stack_new(SC_REF(sc_donated), true);
/* now do the actual donation */
schedContext_donate(sc_donated, tcb_callee);
@ -64,27 +63,24 @@ void reply_pop(reply_t *reply, tcb_t *tcb)
word_t next_ptr = call_stack_get_callStackPtr(reply->replyNext);
word_t prev_ptr = call_stack_get_callStackPtr(reply->replyPrev);
if (likely(next_ptr != 0)) {
assert(call_stack_get_isHead(reply->replyNext));
SC_PTR(next_ptr)->scReply = REPLY_PTR(prev_ptr);
if (prev_ptr != 0) {
REPLY_PTR(prev_ptr)->replyNext = reply->replyNext;
assert(call_stack_get_isHead(REPLY_PTR(prev_ptr)->replyNext));
}
SC_PTR(next_ptr)->scReply = REPLY_PTR(prev_ptr);
if (prev_ptr != 0) {
REPLY_PTR(prev_ptr)->replyNext = reply->replyNext;
assert(call_stack_get_isHead(REPLY_PTR(prev_ptr)->replyNext));
}
reply->replyNext = call_stack_new(0, false);
/* give it back */
if (tcb->tcbSchedContext == NULL) {
/* only give the SC back if our SC is NULL. This prevents
* strange behaviour when a thread is bound to an sc while it is
* in the BlockedOnReply state. The semantics in this case are that the
* SC cannot go back to the caller if the caller has received another one */
schedContext_donate(SC_PTR(next_ptr), tcb);
}
/* give it back */
if (tcb->tcbSchedContext == NULL) {
/* only give the SC back if our SC is NULL. This prevents
* strange behaviour when a thread is bound to an sc while it is
* in the BlockedOnReply state. The semantics in this case are that the
* SC cannot go back to the caller if the caller has received another one */
schedContext_donate(SC_PTR(next_ptr), tcb);
}
reply->replyPrev = call_stack_new(0, false);
reply->replyNext = call_stack_new(0, false);
reply_unlink(reply, tcb);
}