Searched refs:tcb_callee (Results 1 - 2 of 2) sorted by relevance

/seL4-mcs-10.1.1/include/object/
H A Dreply.h32 void reply_push(tcb_t *tcb_caller, tcb_t *tcb_callee, reply_t *reply, bool_t canDonate);
/seL4-mcs-10.1.1/src/object/
H A Dreply.c15 reply_push(tcb_t *tcb_caller, tcb_t *tcb_callee, reply_t *reply, bool_t canDonate) argument
23 if (tcb_callee->tcbSchedContext) {
37 thread_state_ptr_set_replyObject(&tcb_callee->tcbState, 0);
45 assert(tcb_callee->tcbSchedContext == NULL);
62 schedContext_donate(sc_donated, tcb_callee);

Completed in 75 milliseconds