- Devel - lists.sel4.systems

Re: [seL4] Cross-core thread migration
by Millar, Curtis (Data61, Kensington NSW) 09 Apr '20

09 Apr '20

On Tue, 2020-04-07 at 12:00 +1000, devel-request(a)sel4.systems wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > 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 > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > 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 <anna(a)gh.st> > To: laokz <laokz(a)foxmail.com>, devel <devel(a)sel4.systems> > Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo > Message-ID: > < > BYAPR13MB22292529DC4150329B0C44E6DCC20(a)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 <demiobenour(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Cross-core thread migration > Message-ID: > < > CAJEMUN_it3Uf4Bhs3dVvfLRPeQvznJ8BCJ+Rq2wLbqcLDDHyCw(a)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 > Devel(a)sel4.systems > 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

1 0

Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo
by laokz 09 Apr '20

09 Apr '20

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(a)gh.st>; Date: Mon, Apr 6, 2020 12:16 PM To: "laokz"<laokz(a)foxmail.com>;"devel"<devel(a)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.

2 1

The seL4 Foundation is up!
by Heiser, Gernot (Data61, Kensington NSW) 08 Apr '20

08 Apr '20

See my announcement: https://sel4.systems/pipermail/announce/2020/000027.html My blog explains the reasons for it and what we want it to achieve: https://microkerneldude.wordpress.com/2020/04/07/the-sel4-foundation-what-a… And we really want to increase community engagement: here there are plenty of places to contribute: https://docs.sel4.systems/projects/available-user-components.html Gernot on behalf of all of us at Trustworthy Systems

1 0

Cross-core thread migration
by Demi Obenour 06 Apr '20

06 Apr '20

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

1 0

setConsumed() in seL4_SchedContext_YieldTo
by laokz 06 Apr '20

06 Apr '20

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

2 1

CAmkES, Virtual Machines and Multicore Guarantees
by Demi M. Obenour 01 Apr '20

01 Apr '20

> On 18 Mar 2020, at 10:13, Demi Obenour <demiobenour(a)gmail.com> wrote: > > On Tue, Mar 17, 2020, 9:29 PM Klein, Gerwin (Data61, Kensington NSW) < > Gerwin.Klein(a)data61.csiro.au> wrote: > >> >> >> > On 18 Mar 2020, at 08:59, Demi Obenour <demiobenour(a)gmail.com> wrote: >> > >> > On Tue, Mar 17, 2020, 7:32 PM Mcleod, Kent (Data61, Kensington NSW) < >> > Kent.Mcleod(a)data61.csiro.au> wrote: >> > >> > The closest you could get to a multicore system that leverages verified >> >> kernel configurations would be to setup a multikernel implementation >> where >> >> each core had its own instance of a verified seL4 configuration where >> any >> >> hardware resources are strictly partitioned between them. I'm not >> aware of >> >> any examples of this setup but there have been research projects that >> have >> >> used multikernel implementations of seL4 in the past. Also this still >> >> wouldn't give you an overall system with the same guarantees as a >> single >> >> seL4 as the different instances would need to trust each other to not >> >> overwrite each other's kernel data structures and is outside of the >> current >> >> proof assumptions. >> >> >> > >> > Assuming that the root tasks drop capabilities that could be >> problematic, >> > would this still be correct? This seems to follow from the existing >> seL4 >> > specification (no way to get rights to memory from nothing). >> >> You can set up a system to be completely separated from the root task, >> and yes, that would increase confidence. There was a PhD thesis a while ago >> that had a semi-formal but fairly rigorous argument for why and how this >> will work, but you’d still not be running the verified configuration of the >> kernel, i.e. you’d have code in there that was not verified, even if that >> code doesn’t do much in this setup and you can probably convince yourself >> manually that it is fine. >> > > Since the code is deterministic, and will only ever have one initial > condition, is it possible to prove it correct by simply running the binary > and looking at the state after it executes? That is, this code could be > viewed as an extension of the kernel init code. > > > That would work per system, yes, although you’d have to re-do that > certification every time you tweaked something in the setup of that system. > > We’ve thought about this approach also for kernel initialisation in > general, i.e. writing an automated check that the invariants are true after > the system is initialised. There are a lot of expensive calculations in > that check, though, so we haven’t really gone with that. Still remains an > option, though. (Expensive, because the invariants have things like “for > every cap, if there exists another cap to the same object, this cap must > have the following properties” etc, ie. lots of forall/exists combinations > over all of memory, which are no problem in logic, but hard on > computation). > > You’d also still have kernel code that runs later that is not verified, > mostly very simple stuff such as instead of a current thread, you have an > array of current threads (one per CPU). The PhD thesis[1] did look at that > and concluded it’s all fine, but compared to a full code-level verification > that’s obviously lower assurance. The thesis is from 2013, so a lot has > happened since then, but the general idea still holds. > > [1]: > https://ts.data61.csiro.au/publications/nictaabstracts/vonTessin:phd.abstra… > > > > > Also, why is verifying fine-grained locking so difficult? CertiKOS >> managed >> > to do it, so I am probably missing something. >> >> I don’t see that much fine-grained locking in CertKOS, it mostly uses >> separation. It’s easier for it to do so, because it has a significantly >> simpler API (in fact, it’s probably quite similar to a multikernel setup in >> seL4 + messaging between cores. The only setups I’ve seen have precisely >> one VM per core). >> > > I was not aware of that, thank you. > > > It seems to be even worse, actually -- according to the paper that Gernot > posted there is no communication between cores, which if I think back to > the projects I’ve seen is actually true there as well, they used shared > memory between VMs to communicate, not kernel primitives. It also has > cooperative scheduling which is fine for some systems, but not others. It’s > notoriously hard to figure out what features CertiKOS actually has, because > the papers of course concentrate on other aspects such as verification (as > do ours, it’s probably not that easy to figure out what is verified in > which version of seL4 either without a lot of reading, but we do try to be > explicit about it :-)). > > Gernot is obviously not very happy with them from a systems perspective. > From the verification side, they have done some pretty cool things, just > not to the systems level that Gernot would find acceptable ;-) > > > Thank you so much. I view seL4 as universal, in that it should be > possible to build virtually any desired OS on top of it, and I am glad that > a high-performance multicore version with fine-grained locking at least > appears feasible. > > > It’s definitely part of the vision. There is a lot of thinking about > fine-grained vs big-lock, because the seL4 big-lock is about the order of a > Linux fine-grained lock, with some caveats, but the idea is that we want > this to scale. Is it planned to scale beyond the area of small inter-core communication costs? Obviously, transferring large amounts of data between cores on hot paths won't scale. However, I am still not convinced that a multikernel is the best way to go: it has always seemed like a hack to work around kernel limitations, and it seems to make slow-path control-plane userspace code far more complex. Such code often isn't performance critical at all, so forcing it to be distributed seems like unnecessary complexity. Furthermore, replicating data structures (such as page tables) which are almost entirely read-only seems like it could create substantial overhead, although I am not sure if that is an issue in practice. Finally, as someone who writes Rust professionally, I find thread-affine APIs to be quite annoying to deal with. Resources that can't be safely accessed by more than one thread concurrently are easy to wrap in clean APIs, but resources that can't be sent across threads are much harder to wrap. Making kernel resources specifically per-core, and preventing them from being transferred between cores, seems likely to lead to a bunch of userspace frameworks of varying quality that try to work around this limitation. > Are there any papers that I could read to learn more? > > > We don’t have anything really published yet on the verification side, > because it’s all still ongoing work. There is one about the big-lock idea, > though: > > https://ts.data61.csiro.au/publications/nictaabstracts/Peters_DEH_15.abstra… I read and like that idea. My biggest worry, however, is that a big lock won't scale beyond a small number of cores. The idea that fine-grained locking might be possible to verify gives me hope, as I had previously given up on that. > Cheers, > Gerwin Cheers, Demi=

2 1

Get/Set multiple message registers with the one syscall?
by Ben Ph 01 Apr '20

01 Apr '20

I'm looking at `seL4_GetMR()` and `seL4_SetMR()`, which requires a syscall for each get/set. To my naive eye, it seems like you're much better off running `seL4_GetIPCBuffer()->msg` then reading/writing to each index as needed, turning multiple syscalls (one for each get/set) into just the one. Am I missing anything? I was planning on replacing my Get/Set calls with direct array writes, but I'm wondering if I've missed reasons why I shouldn't. Thanks, Ben

2 2

Running cmakes-arm-vm under QEMU.
by Travis Wheatley 01 Apr '20

01 Apr '20

Greetings sel4 developers. Thus far I have successfully been able to build and boot the cmakes-arm-vm project on a Jetson TK1 board. However, my project requires a 64 bit target. I have built the TX1 version of this project but unfortunately do not have a TX1 board to try it out on. I would like to be able to run under QEMU but am not quite sure how to assemble all of the bits needed to do so. I believe what I need is a raw kernel image, a ramdisk, and a dtb file but not sure how to extract these in the proper formats from the files produced in the build process. Is there any existing documentation or guidance that can help me get a 64 bit buildroot kernel running under an sel4 vm to boot under QEMU? — Travis

2 1

Thank you very much. 答复: question about stash and pop between templates
by yadong.li 23 Mar '20

23 Mar '20

-----邮件原件----- 发件人: Matthew Fernandez [mailto:matthew.fernandez@gmail.com] 发送时间: 2020年3月22日 2:00 收件人: yadong.li 抄送: devel(a)sel4.systems 主题: Re: [seL4] question about stash and pop between templates I think I wrote the text you’re quoting, so I’ll attempt an answer. In connection templates, ‘me’ is not unique. I can’t remember exactly how this works, but ‘me’ either refers to the component instance of the end of the template you’re instantiating or to the connection itself. If you want to try and unravel the relevant code, it’s around lines 278-300 of the main function [0]. The ‘stash’ and ‘pop’ functions were implemented to expose some internals to advanced CAmkES users who wanted functionality beyond the template API. They were not widely used, and many of these users sidestepped them and used the even more questionable ‘_stash’ and ‘_pop’ variants. I would not be surprised if they do not work the way the documentation describes, and they should mostly be considered foot guns at this point. This is based on my ~5 year old memories so may be inaccurate or out of date. HTH [0]: https://github.com/seL4/camkes-tool/blob/master/camkes/runner/__main__.py#L… > On Mar 20, 2020, at 22:56, yadong.li <yadong.li(a)horizon.ai> wrote: > > Hi， > Recently, I try to learning about CMAKES > I have some question about stash and pop described as followes: > > “ > Passing Information Between Templates > You often wish to do this with two related templates. For example, in the templates that form each side of a connection you often wish to talk about the same object on both sides. None of the templates currently call the low-level helper functions that enable this directly, but if you do want to invoke them, they are stash and pop. stash lets you save a Python object under a given key name and pop retrieves a previously saved Python object by key. Note that these are only usable for passing objects between templates that share related me references.” > What is the meaning of “between templates that share related me references.” ? > It is my understanding that template will be instantiated, every instance has its own ‘me’ , for example below: > connection seL4VirtQueues ping_virtq_conn1(to ping_vqinit1.init, from > ping_client.recv, from vm0.send1); To parse the AST, seL4VirtQueues-from.template.c will be called twice for ping_client.recv and vm0.send1, I think they should have their own ‘me’ > where can I found the code to share related ‘me’ between the instance. > > Thanks for your answer _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel

1 0

question about stash and pop between templates
by yadong.li 22 Mar '20

22 Mar '20

Hi， Recently, I try to learning about CMAKES I have some question about stash and pop described as followes: “ Passing Information Between Templates You often wish to do this with two related templates. For example, in the templates that form each side of a connection you often wish to talk about the same object on both sides. None of the templates currently call the low-level helper functions that enable this directly, but if you do want to invoke them, they are stash and pop. stash lets you save a Python object under a given key name and pop retrieves a previously saved Python object by key. Note that these are only usable for passing objects between templates that share related me references.” What is the meaning of “between templates that share related me references.” ? It is my understanding that template will be instantiated, every instance has its own ‘me’ , for example below: connection seL4VirtQueues ping_virtq_conn1(to ping_vqinit1.init, from ping_client.recv, from vm0.send1); To parse the AST, seL4VirtQueues-from.template.c will be called twice for ping_client.recv and vm0.send1, I think they should have their own ‘me’ where can I found the code to share related ‘me’ between the instance. Thanks for your answer

2 1