On Tue, 2020-04-07 at 12:00 +1000, [email protected] wrote: > Send Devel mailing list submissions to > [email protected] > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > [email protected] > > You can reach the person managing the list at > [email protected] > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Re: setConsumed() in seL4_SchedContext_YieldTo (Anna Lyons) > 2. Cross-core thread migration (Demi Obenour) > > > ------------------------------------------------------------------- > --- > > Message: 1 > Date: Mon, 6 Apr 2020 04:16:00 +0000 > From: Anna Lyons <[email protected]> > To: laokz <[email protected]>, devel <[email protected]> > Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo > Message-ID: > < > byapr13mb22292529dc4150329b0c44e6dc...@byapr13mb2229.namprd13.prod.outlook.com > > > > Content-Type: text/plain; charset="iso-8859-1" > > 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. > > > > 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. > > > ------------------------------ > > Message: 2 > Date: Mon, 6 Apr 2020 02:23:08 -0400 > From: Demi Obenour <[email protected]> > To: [email protected] > Subject: [seL4] Cross-core thread migration > Message-ID: > < > cajemun_it3uf4bhs3dvvflrpeqvznj8bcj+rq2wlbqclddh...@mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > If I have a manycore machine, what is the best way to migrate a > thread from > one core to another? Similarly, how can I send a capability (such as > to > memory)? Cryptography is an option for the second one, but seems > inelegant > and inefficient. Alternatively, are future versions of seL4 expected > to > scale to manycore systems without needing a multikernel? That would > presumably make the answer trivial. > > Sincerely, > > Demi > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > [email protected] > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 71, Issue 6 > ************************************
Hi Demi, > If I have a manycore machine, what is the best way to migrate a thread from > one core to another? Similarly, how can I send a capability (such as to > memory)? Cryptography is an option for the second one, but seems inelegant > and inefficient. When configured with SMP (which is not currently available in any verified config urations) a thread can be migrated to another core within a single kernel image cluster by changing its affinity. The MCS API will change this slightly; each scheduling context is associated with a core of the kernel image cluster so the scheduling context can be reconfigured to run on a different core (using that core's ScheduleControl capability) or a scheduling context already associated with that core can be bound to the thread to move it to that core. > Alternatively, are future versions of seL4 expected to > scale to manycore systems without needing a multikernel? That would > presumably make the answer trivial. IPC between cores in a single kernel image provides all of the necessary mechanisms for transferring data and capabilities between threads. In larger multicore machines, the cores would be split up into clusters where each cluster would essentially map to a single shared L2 cache (more generally, the clusters would be split to keep accesses to shared data structures in the kernel in the higher-level caches). I'm not sure how we would approach transferring kernel objects and capabilities between kernel images on different clusters whilst preserving the particular design goals that seL4 aims to implement. Cheers, Curtis _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
