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
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
