Hello, In kernel/src/object/schedcontext.c, setConsumed(sched_context_t *sc, word_t *buffer) does reset sc->scConsumed and overwrite ksCurThread-
msgRegisters[0] no matter who calls it. So in my understanding, it should be called only once in a syscall path, otherwise prior call info must lost.
seL4_SchedContext_YieldTo's actual function invokeSchedContext_YieldTo() has the beginning: ``` if (sc->scYieldFrom) { schedContext_completeYieldTo(sc->scYieldFrom); assert(sc->scYieldFrom == NULL); } ``` and at its end: ``` if (return_now) { setConsumed(sc, buffer); } ``` Because schedContext_completeYieldTo actually called setConsumed(), so here might produce twice calling of setConsumed(). I don't know the practice usage of this method and can't tell it is trivial or not. From coding view, here exists the edge case. Regards, laokz