From fd14374e9dc5723ed6bdbc71f587980cc1b6286c Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Mon, 31 Mar 2025 13:51:35 +1030 Subject: [PATCH] mcs: refactor reply functions to ease verification 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 --- include/kernel/thread.h | 7 +++++++ src/object/reply.c | 36 ++++++++++++++++-------------------- 2 files changed, 23 insertions(+), 20 deletions(-) diff --git a/include/kernel/thread.h b/include/kernel/thread.h index d326ebdff..08689ef14 100644 --- a/include/kernel/thread.h +++ b/include/kernel/thread.h @@ -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 diff --git a/src/object/reply.c b/src/object/reply.c index 82fd4e3ee..9a47575f2 100644 --- a/src/object/reply.c +++ b/src/object/reply.c @@ -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); }