- Devel - lists.sel4.systems

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

Plan to remove support for ARMv6 and KZM/imx31
by Mcleod, Kent (Data61, Kensington NSW) 20 Mar '20

20 Mar '20

We are planning on removing support for the KZM ARM11 platform in order to reduce maintenance burden. We are assuming that this is a dead platform and removing support won't affect anyone but it would be useful to know who if anyone is currently using this platform and how much interest there is in ongoing support. The platform was the original verification target of seL4 over 10 years ago and by now there doesn't appear to be any ways to obtain new hardware. It is starting to require more attention as the physical board we have is starting to intermittently fail independently from the KZM Qemu simulation target. Currently, the KZM platform is the only ARMv6 platform that we support and supporting it requires a few work-arounds for emulating mechanisms that newer hardware supports. Removing this platform also implies removing armv6 support. There is an older discourse topic for discussion on this topic here: https://sel4.discourse.group/t/should-we-continue-to-support-armv6-and-kzm-…

1 0

Would verifying ARM64 be any more difficult than verifying ARM32 was?
by Demi M. Obenour 19 Mar '20

19 Mar '20

Would verifying seL4 on ARM64 be any more difficult than verifying seL4 on ARM32 was? What about other architectures like POWER9? I hope I am not asking too many questions; I am just a curious outsider who hopes they can use seL4 someday. Sincerely, Demi

4 3