RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

mcs: add tcb argument to reply_unlink

Browse Source 
reply_unlink takes a reply and remove the link between that reply
and its tcb. This link always exists at the call site and the tcb
information is always avaialble, or can be made available.

This commit adds this tcb as an extra argument to aid varification.

Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
This commit is contained in:
Miki Tanaka
2020-08-14 22:50:50 +10:00
parent 2ff45c3ca8
commit 4ee1f90a7d
5 changed files with 25 additions and 22 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
include/object/reply.h
View File

@@ -11,12 +11,12 @@
#include <object/structures.h>
/* Unlink a reply from its tcb */
static inline void reply_unlink(reply_t *reply)
static inline void reply_unlink(reply_t *reply, tcb_t *tcb)
{
/* check the tcb and reply are linked correctly */
assert(thread_state_get_replyObject(reply->replyTCB->tcbState) == REPLY_REF(reply));
assert(reply->replyTCB == tcb);
assert(thread_state_get_replyObject(tcb->tcbState) == REPLY_REF(reply));
tcb_t *tcb = reply->replyTCB;
thread_state_ptr_set_replyObject(&tcb->tcbState, REPLY_REF(0));
reply->replyTCB = NULL;
setThreadState(tcb, ThreadState_Inactive);
@@ -25,9 +25,9 @@ static inline void reply_unlink(reply_t *reply)
/* Push a reply object onto the call stack */
void reply_push(tcb_t *tcb_caller, tcb_t *tcb_callee, reply_t *reply, bool_t canDonate);
/* Pop the head reply from the call stack */
void reply_pop(reply_t *reply);
void reply_pop(reply_t *reply, tcb_t *tcb);
/* Remove a reply from the call stack - replyTCB must be in ThreadState_BlockedOnReply */
void reply_remove(reply_t *reply);
void reply_remove(reply_t *reply, tcb_t *tcb);
/* Remove a specific tcb, and the reply it is blocking on, from the call stack */
void reply_remove_tcb(tcb_t *tcb);

2
src/kernel/thread.c
View File

@@ -134,7 +134,7 @@ void doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot, bool_t grant)
}
tcb_t *receiver = reply->replyTCB;
reply_remove(reply);
reply_remove(reply, receiver);
assert(thread_state_get_replyObject(receiver->tcbState) == REPLY_REF(0));
assert(reply->replyTCB == NULL);
#else

6
src/object/endpoint.c
View File

@@ -85,7 +85,7 @@ void sendIPC(bool_t blocking, bool_t do_call, word_t badge,
#ifdef CONFIG_KERNEL_MCS
reply_t *reply = REPLY_PTR(thread_state_get_replyObject(dest->tcbState));
if (reply) {
reply_unlink(reply);
reply_unlink(reply, dest);
}
if (do_call ||
@@ -326,7 +326,7 @@ void cancelIPC(tcb_t *tptr)
#ifdef CONFIG_KERNEL_MCS
reply_t *reply = REPLY_PTR(thread_state_get_replyObject(tptr->tcbState));
if (reply != NULL) {
reply_unlink(reply);
reply_unlink(reply, tptr);
}
#endif
setThreadState(tptr, ThreadState_Inactive);
@@ -381,7 +381,7 @@ void cancelAllIPC(endpoint_t *epptr)
#ifdef CONFIG_KERNEL_MCS
reply_t *reply = REPLY_PTR(thread_state_get_replyObject(thread->tcbState));
if (reply != NULL) {
reply_unlink(reply);
reply_unlink(reply, thread);
}
if (seL4_Fault_get_seL4_FaultType(thread->tcbFault) == seL4_Fault_NullFault) {
setThreadState(thread, ThreadState_Restart);

4
src/object/objecttype.c
View File

@@ -139,10 +139,10 @@ finaliseCap_ret_t finaliseCap(cap_t cap, bool_t final, bool_t exposed)
if (reply && reply->replyTCB) {
switch (thread_state_get_tsType(reply->replyTCB->tcbState)) {
case ThreadState_BlockedOnReply:
reply_remove(reply);
reply_remove(reply, reply->replyTCB);
break;
case ThreadState_BlockedOnReceive:
reply_unlink(reply);
reply_unlink(reply, reply->replyTCB);
break;
default:
fail("Invalid tcb state");

25
src/object/reply.c
View File

@@ -51,14 +51,15 @@ void reply_push(tcb_t *tcb_caller, tcb_t *tcb_callee, reply_t *reply, bool_t can
}
/* Pop the head reply from the call stack */
void reply_pop(reply_t *reply)
void reply_pop(reply_t *reply, tcb_t *tcb)
{
assert(reply != NULL);
assert(reply->replyTCB != NULL);
assert(thread_state_get_tsType(reply->replyTCB->tcbState) == ThreadState_BlockedOnReply);
assert(thread_state_get_replyObject(tcb->tcbState) == REPLY_REF(reply));
assert(reply->replyTCB == tcb);
/* unlink tcb and reply */
tcb_t *tcb = reply->replyTCB;
reply_unlink(reply);
reply_unlink(reply, tcb);
word_t next_ptr = call_stack_get_callStackPtr(reply->replyNext);
word_t prev_ptr = call_stack_get_callStackPtr(reply->replyPrev);
@@ -87,9 +88,11 @@ void reply_pop(reply_t *reply)
}
/* Remove a reply from the middle of the call stack */
void reply_remove(reply_t *reply)
void reply_remove(reply_t *reply, tcb_t *tcb)
{
assert(thread_state_get_tsType(reply->replyTCB->tcbState) == ThreadState_BlockedOnReply);
assert(reply->replyTCB == tcb);
assert(thread_state_get_tsType(tcb->tcbState) == ThreadState_BlockedOnReply);
assert(thread_state_get_replyObject(tcb->tcbState) == REPLY_REF(reply));
word_t next_ptr = call_stack_get_callStackPtr(reply->replyNext);
word_t prev_ptr = call_stack_get_callStackPtr(reply->replyPrev);
@@ -97,15 +100,15 @@ void reply_remove(reply_t *reply)
if (likely(next_ptr)) {
if (likely(call_stack_get_isHead(reply->replyNext))) {
/* head of the call stack -> just pop */
reply_pop(reply);
reply_pop(reply, tcb);
return;
}
/* not the head, remove from middle - break the chain */
REPLY_PTR(next_ptr)->replyPrev = call_stack_new(0, false);
reply_unlink(REPLY_PTR(reply));
} else if (reply->replyTCB) {
reply_unlink(REPLY_PTR(reply), tcb);
} else {
/* removing start of call chain */
reply_unlink(reply);
reply_unlink(reply, tcb);
}
if (prev_ptr) {
@@ -137,5 +140,5 @@ void reply_remove_tcb(tcb_t *tcb)
reply->replyPrev = call_stack_new(0, false);
reply->replyNext = call_stack_new(0, false);
reply_unlink(reply);
reply_unlink(reply, tcb);
}