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