Hi laokz,

Yes, that scenario cannot happen. If B runs to block, and A is scheduled, the kernel will complete A's initial yieldTo call and clear the appropriate values before resuming A.

Cheers Anna. ________________________________ From: laokz laokz@foxmail.com Sent: Wednesday, 8 April 2020 11:32 PM To: Anna Lyons anna@gh.st; devel devel@sel4.systems Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo

Hello Anna,

Thanks for the reply. Maybe I'v imagined an impractical scenario:

1. A yield to B. B->sc->scYieldFrom=A

2. B run then block.

3. A run then yield to B again.

4. Now at the beginning, setConsumed() called; because B is not runnable, so return_now=true and setConsumed() called again at the end.

For cooperative threads, this indeed shouldn't happen but it depends. For example if B can block, then great care should be taken to forbid this edge case.

Regards, laokz

------------------ Original ------------------ From: "Anna Lyons"anna@gh.st; Date: Mon, Apr 6, 2020 12:16 PM To: "laokz"laokz@foxmail.com;"devel"devel@sel4.systems;

Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo

P {margin-top:0;margin-bottom:0;} Hi,

Thanks for the observation! It's true that setConsumed should only be called once per kernel entry, and it's not obvious just from the code snippets to observe that this is true.

However, the semantics of YieldTo mean that both of these code paths cannot be executed in the same kernel entry.

If return_now is true, this means that the current thread will be switched to and sc->scYieldFrom should be NULL (as the YieldTo call has completed). This is usually the case if the calling thread YieldTo a lower priority thread, or a thread that is not runnable. On the other hand if return_now is false, the YieldTo resulted in the thread being YieldedTo being switched to, so we return the result of the YieldTo on a different kernel entry (when we run the thread that called YieldTo again).

With this context, take a look at the if block here: https://github.com/seL4/seL4/blob/master/src/object/schedcontext.c#L191 Where you can see that we only set sc->scYieldFrom when we also set return_now to false.

Glad to see someone looking at the MCS kernel.

Anna. ________________________________

WARNING This email originates from an e-mail address outside of Ghost Locomotion. Do not open attachments or click links unless you are sure this email comes from a known, trusted sender.

________________________________

Confidentiality Note:This email is intended only for the person or entity to which it is addressed and may contain information that is privileged, confidential or otherwise protected from disclosure. Unauthorized use, dissemination, distribution or copying of this email or the information herein by anyone other than the intended recipient is strictly prohibited. If you have received this email in error, please notify the sender immediately and destroy the original message, any attachments thereto and all copies.