- Devel - lists.sel4.systems

Incorporating the Build System - The CAmkES Perspective
by Turner, Ben 20 Apr '20

20 Apr '20

Hi, We are attempting to define a system that comprises 3 components that can talk to each other. We have managed to get the system built and working using the existing tutorial repo and the hello-camkes-0 app, however we are struggling to determine what precisely we would need to copy from this in order to define our own standalone application within the seL4 build system. We have read the existing documentation at https://docs.sel4.systems/projects/buildsystem/incorporating.html but cannot find any information on what additions are required when using the CAmkES and ARM capabilities. Any help you can provide would be appreciated. Kind regards, Ben Turner ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

2 1

TimeServer "IRQ already mapped" error
by Grant Jurgensen 17 Apr '20

17 Apr '20

Hi all, I'm trying to add a timer to my CAmkES component (all I need is a timestamp). I've been using this example component as a reference: https://github.com/seL4/camkes/tree/master/apps/timeserver My problem is that when I declare an instance of the global TimeServer component in my ".camkes" file, I get an error at build-time: "parse-capDL: IRQ already mapped: 68". I'm not sure what to make of this error. The only major difference between my project and the reference above is that I am building atop the camkes-arm-vm project. Could the VM be interfering here? Thanks, Grant Jurgensen

2 3

Benchmarks of seL4
by Leo Gaspard 16 Apr '20

16 Apr '20

Hello, I come wondering: the FAQ claims that seL4 is “the world's fastest microkernel”. However, I can only find benchmarks of just seL4, without comparison to other operating systems running on the same machine. Would you happen to have such comparative benchmarks? I'd be particularly interested by something against L4Re, as it'd probably allow me to guess at the performance of something similar to L4Linux ported to seL4. Thank you for all you do on seL4! Leo

6 12

Failed to find device frame in new verion on my environment
by yadong.li 16 Apr '20

16 Apr '20

Hi， I recently move my wrok to a new seL4 version (I checkout default.xml in project camkes-arm-vm on 2020.02.25), I have below error print: “create_object@main.c:659 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0x90006000” 1、 I debug code, /**/ is my environment run parameter BOOT_CODE bool_t create_device_untypeds(cap_t root_cnode_cap, seL4_SlotPos slot_pos_before) { paddr_t start = 0; /*---------------------add region, start = 0x1800000, end = 0x2080000 *---------------------add region, start = 0x20ff000, end = 0x2100000 *---------------------add region, start = 0x80000000, end = 0x90001000 *---------------------add region, start = 0x90003000, end = 0x90004000 */ for (word_t i = 0; i < ndks_boot.resv_count; i++) { if (start < ndks_boot.reserved[i].start) { region_t reg = paddr_to_pptr_reg((p_region_t) { start, ndks_boot.reserved[i].start }); if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) { return false; } } start = ndks_boot.reserved[i].end; } /*---------------------add region, start = 0x90005000, CONFIG_PADDR_USER_DEVICE_TOP = 0xff, PPTR_TOP = 0xffffc0000000*/ if (start < CONFIG_PADDR_USER_DEVICE_TOP) { region_t reg = paddr_to_pptr_reg((p_region_t) { start, CONFIG_PADDR_USER_DEVICE_TOP }); /* * The auto-generated bitfield code will get upset if the * end pptr is larger than the maximum pointer size for this architecture. */ if (reg.end > PPTR_TOP) { reg.end = PPTR_TOP; } if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) { return false; } } return true; } 2、 CONFIG_PADDR_USER_DEVICE_TOP = 0xff, I found print the value must use 0x%x, can’t use 0x%lx, it is wrong 3、My platform is cortexA53 kernel/src/plat/j2/config.cmake:28: set(KernelArmCortexA53 ON) 4、and I change follow KernelArmCortexA53： a) ‘math(EXPR KernelPaddrUserTop "(1 << 40) - 1")’ to ‘set(KernelPaddrUserTop "1099511627775")’ ----------the print is “Failed to find device frame” disappear 5、my pc tools install，follow the seL4 wiki， cmakes version is 3.12.2 (> 3.7.2) 6、I did not find error or warning when I ../init-build.sh -DAARCH64=TRUE …… ---------------is it need to install new tools? Or other problem Thank you very much.

2 1

RPi4: DTS memory device and vm_minimal
by Turner, Ben 16 Apr '20

16 Apr '20

Hi, I have been attempting to get the vm_minimal application running on the Raspberry Pi 4 platform, and I have managed to get to the point where I need to define the memory regions for the kernel and virtual machine. The issue is that I do not know what the correct values (if any) would be needed in the overlay-rpi4.dts that I have created. From what I have found to this point, the Pi platform implements a memory system that means it is not possible to define memory regions in a DTS file. These memory regions are user-defined and are not known until runtime. I think I know what the answer will be to this; is there a way to overcome the oddities of the RPi4 memory setup when attempting to create a seL4 CAmkES VM linux image? Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner(a)roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

2 3

Trouble booting default cmakes-vm-arm project under QEMU
by Travis Wheatley 16 Apr '20

16 Apr '20

Sel4 Developers, Still learning to crawl here. I have built the cmakes-vm-arm project for the qemu-arm-virt target. I have QEMU version 3.1.0 installed on my host. When I run the simulation by executing the command “./simulate”. it appears as though Sel4 is booting and successfully downloading the kernel, dtb, and loader. However, I am running into problems when it starts booting the kernel. It looks to me like it might be booting the kernel OK with the exception of a warning about GIC interrupts and subsequently drops to user space. Following that I see errors about insufficient memory and invalid num_vcpus. Not quite sure how to correct this. Hoping one of y’all can point me in the right direction. Here is a copy of the output — Begin included text — $ ./simulate ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61b01000..62edd947] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61bf7400. Loaded DTB from 61bf7400. paddr=[60239000..6023afff] ELF-loading image 'kernel' paddr=[60000000..60238fff] vaddr=[ff8060000000..ff8060238fff] (my_virtual_env) trickdev@trickvm ~/cmakes-arm-vm/vm-build $ ./simulate ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61b01000..62edd947] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61bf7400. Loaded DTB from 61bf7400. paddr=[60239000..6023afff] ELF-loading image 'kernel' paddr=[60000000..60238fff] vaddr=[ff8060000000..ff8060238fff] virt_entry=ff8060000000 ELF-loading image 'capdl-loader' paddr=[6023b000..61703fff] vaddr=[400000..18c8fff] virt_entry=407fe8 Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/216 T0xff80bf815400 "rootserver" @400704]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> run(a)main.c<mailto:run@main.c>:1095 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1) sel4platsupport_copy_irq_cap(a)device.c<mailto:sel4platsupport_copy_irq_cap@device.c>:41 Failed to get cap for irq irq_register_common(a)irq.c<mailto:irq_register_common@irq.c>:316 Failed to register an IRQ Assertion failed: (cspace->bitmap[index / BITS_PER_WORD] & BIT(index % BITS_PER_WORD)) == 0 (/home/trickdev/cmakes-arm-vm/projects/seL4_libs/libsel4allocman/src/cspace/single_level.c: _cspace_single_level_free: 100)

2 1

Best starting point for running VM Linux on a raspberry pi?
by Travis Wheatley 16 Apr '20

16 Apr '20

Greetings sel4 developers. Thus far I have successfully built and run the camkes-arm-vm on a TK1 platform as described here:https://docs.sel4.systems/projects/camkes-arm-vm/ I have also been able to boot to a u-boot prompt and run some sel4 test code as described here:https://docs.sel4.systems/Hardware/Rpi3.html My goal is to run a custom linux kernel under sel4 on the raspberry pi and am wondering what would be the best starting point. There is a tutorial about running a linux kernel under sel4 located here:https://docs.sel4.systems/Tutorials/camkes-vm-linux.html However, it only supports x86. There is also the camkes-arm-vm mentioned above but the raspberry pi is not among the supported platforms. Before reinventing the wheel I am hoping there might be some existing project or a better starting point for running a linux guest under sel4 on a raspberry pi that I can use. — Travis

2 1

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

13 Apr '20

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

3 4

Support for 64-bit virtual machines on x86-64
by J Call 12 Apr '20

12 Apr '20

Hi all, I’m trying to use seL4 as a hypervisor on an embedded system. This particular SBC has 32 Gb of RAM and I’d like to install a couple of CentOS 8 64bit VMs side by side, but would like the vm’s to take advantage of more than 4Gb of RAM. Is there any word on seL4 supporting 64-bit virtual machines on the x86-64 architecture one day? Sincerely, Jonathan

2 1

Scheduler discussion on LWN
by Zach Lym 12 Apr '20

12 Apr '20

Red Hat's lead real-time scheduling engineer (who has a solid background in formal methods) posted an interested comment on an LWN article about seL4's scheduler research (https://lwn.net/Articles/745946/) While I disagree with the tone of the comment, I rarely see informed critiques of seL4 and context switching performance is core to microkernel viability. My apologies if this is an inappropriate venue for this discussion. --- "With the current scheduler, that driver must be given a high priority and trusted to not hog the CPU." So, they need to implement either RT throttling or the CBS, like Linux. "Another problem is data structures that are shared between criticalities....se of the priority-ceiling protocol can help." Nice, then they will see that the priority ceiling will add release jitter to the highest priority task, and then will notice that they will have to use other protocol, like, mutexes with priority inheritance? Where did I hear about it already... ah! On Linux! It is widely known that if you use priority ceiling, you will have scheduling "latency." But it really helps to reduce the response time... so, what do you prefer Response Time or Scheduling latency (release jitter or any scheduling delay, scheduler overhead... or any other name people do for it)? "Any process that exceeds its CPU budget during a given period can be throttled. Processes that have shorter periods are given a higher priority by the scheduler." Ok! here they have something like CBS, but they are using the fixed-priority rate monotonic scheduling approach! Nice! that is a technology from... 1969? But wait, if they already implemented this, why is the "network driver" a problem? - answer: because they cannot estimate the period of the packets arriving - RM is not flexible enough to all real-world cases! But that does not mean that this is the only solution. So my question is: Is there a sufficient & necessary schedulability test for their scheduler? "what happens if the client's budget runs out while the server is running?" Welcome to our world, check the "dl_boosted" variable on sched_deadline. "This new scheduler solves the problem, but it does not come for free: interrupt latency increases by 11% and scheduling itself is 19% more expensive. In both cases, the need to reprogram hardware timers is the source of most of the slowdown. But, he noted, scheduling in seL4 is "still an order of magnitude faster than Linux"" Welcome to our world again! And let me guess when you will start to have our numbers... When you finish implementing "some memory-management unit operations, and multicore operation"? Because on PREEMPT_RT we do this in microseconds, will they implementation continue working on ns (i.e., an order of magnitude faster than Linux) with such features? And I wonder, where is the mixed-criticality part of the schedulers...? Running Linux as a guest? I read the papers, and the work is very nice! Seriously! Very nice! But please, stop the comparison of orange and apples. It is not possible to compare this OS with Linux. Moreover, there are other OSs with such features running on real systems. Verified or not, they are certified for it.

2 1

答复: Devel Digest, Vol 71, Issue 10
by yadong.li 10 Apr '20

10 Apr '20

Subject: [seL4] TimeServer "IRQ already mapped" error Maybe the irq of Time exist in vm and TimeServer meanwhile. Try delete the tree node of time in your devices.camkes of you platform, like this: assembly { vm0.dtb = dtb([{}]); /*vm0.dtb = dtb([{"path": "/soc/serial@0xA5000000"}]);*/ -----only delete the conflict part } -----邮件原件----- 发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 devel-request(a)sel4.systems 发送时间: 2020年4月10日 10:00 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 71, Issue 10 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 (=?utf-8?B?bGFva3o=?=) 2. TimeServer "IRQ already mapped" error (Grant Jurgensen) ---------------------------------------------------------------------- Message: 1 Date: Thu, 9 Apr 2020 19:11:14 +0800 From: "=?utf-8?B?bGFva3o=?=" <laokz(a)foxmail.com> To: "=?utf-8?B?QW5uYSBMeW9ucw==?=" <anna(a)gh.st>, "=?utf-8?B?ZGV2ZWw=?=" <devel(a)sel4.systems> Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo Message-ID: <tencent_C27271A3F0A40CF84A7FDBB4F299EB059A09(a)qq.com> Content-Type: text/plain; charset="utf-8" Hello Anna, With your point, I am cleared - activateThread() does the completeYieldTo assurance before A yield to B again. Can I conclude that YieldTo() method is limited to 1:1 relationship? Thanks, laokz ------------------ Original ------------------ From: "Anna Lyons"<anna(a)gh.st>; Date: Thu, Apr 9, 2020 07:12 AM 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 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(a)foxmail.com> Sent: Wednesday, 8 April 2020 11:32 PM To: Anna Lyons <anna(a)gh.st>; devel <devel(a)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(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. ------------------------------ Message: 2 Date: Thu, 9 Apr 2020 09:48:49 -0500 From: Grant Jurgensen <gajurgensen(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] TimeServer "IRQ already mapped" error Message-ID: <CAGJ6_3Cdhk9BrMD0roaCZvi7QZr1M7U3GA1jQ3=m0tMHaThSew(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" Hi all, I'm trying to add a timer to my CAmkES component (all I need is a timestamp). I've been using this example component as a reference: https://github.com/seL4/camkes/tree/master/apps/timeserver My problem is that when I declare an instance of the global TimeServer component in my ".camkes" file, I get an error at build-time: "parse-capDL: IRQ already mapped: 68". I'm not sure what to make of this error. The only major difference between my project and the reference above is that I am building atop the camkes-arm-vm project. Could the VM be interfering here? Thanks, Grant Jurgensen ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 71, Issue 10 *************************************

1 0

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

09 Apr '20

Hello Anna, With your point, I am cleared - activateThread() does the completeYieldTo assurance before A yield to B again. Can I conclude that YieldTo() method is limited to 1:1 relationship? Thanks, laokz ------------------ Original ------------------ From: "Anna Lyons"<anna(a)gh.st>; Date: Thu, Apr 9, 2020 07:12 AM 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 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(a)foxmail.com> Sent: Wednesday, 8 April 2020 11:32 PM To: Anna Lyons <anna(a)gh.st>; devel <devel(a)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(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.

1 0

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 21 Mar '20

21 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

CAmkES, Virtual Machines and Multicore Guarantees
by Turner, Ben 18 Mar '20

18 Mar '20

Hi, In the seL4 FAQ section it states: "Multicore is presently supported on x64 and Arm v7 (32-bit) and v8 (64-bit). Verification of the multicore kernel is in progress (but presently as an unfunded background activity)." Considering only seL4 ----------------------------- My interpretation of this is that given a single seL4 application running on a device, it is not possible to currently guarantee the protections seL4 provides if the application invokes multiple threads across more than 1 core. Is this correct? Considering CAmkES ---------------------------- I would also like to know how CAmkES affects this. For example, looking at the vm_multi app for the exynos5422 in the camkes-arm-vm repository, what would the effect be of assigning unique CPU affinities to each of the VM components? Do the guarantees still hold in this situation? Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner(a)roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

5 4

Configuring pinmux in am335x (beaglebone) can't be done from user mode
by Stephen Sherratt 18 Mar '20

18 Mar '20

Hi all, I've been experimenting with seL4 running on a Ninjablocks (https://www.engadget.com/2013/05/01/ninja-blocks/) that I had lying around. Inside there is a beaglebone, with a custom shield (or cape) containing a microcontroller (atmega328p), some LEDs and a radio. The beaglebone (which normally runs linux) sends json-encoded commands over a serial connection to the on-cape microcontroller, which runs firmware that decodes these commands and controls the LEDs and radio. The complication is that the am335x pins connected to the custom shield are multiplexed, and don't connect to a uart device by default (they are gpio pins by default). The "Control Module" in the am335x can be used to configure pin multiplexing, but it can't be written to in user-mode. From the am335x manual (http://www.ti.com/lit/ug/spruh73q/spruh73q.pdf, page 1449): "Note: For writingto the controlmoduleregisters,the MPUwill need to be in privileged modeof operationand writes will not work fromusermode." To test that the rest of my app works I added the control module to the beaglebone device tree overlay and hacked the kernel to configure the relevant pins to connect to the uart device during boot: https://github.com/stevebob/seL4/commit/4295035ac7fd720fb531b7e0893f1f1191e… And now I have a little rootserver that can control the colours of LEDs on the shield: https://github.com/stevebob/sel4ninja/blob/master/apps/hello-ninja/src/main… What would be the right way of configuring the control module in a seL4-based system, given that it has to happen in kernel mode? To configure the uart pins when running linux on the board, I had to add the following to the device tree: scm@0 { ... pinmux@800 { ... pinmux_uart0_pins { // <-- this was already here pinctrl-single,pins = <0x170 0x30 0x174 0x00>; phandle = <0x20>; }; pinmux_uart1_pins { // <-- I had to add this pinctrl-single,pins = <0x180 0x30 0x184 0x00>; phandle = <0x60>; }; The (seL4) kernel build system already has basic support for interpreting device trees. Would a reasonable solution to my problem be extending this support with a minimal statically-generated control module driver that configures pinmux during boot based on the device tree? There would still be a problem where each board could only have a single pinmux config (as specified by that board's device tree). It seems like an easy fix for this would be a config variable passed to the build system (similar to -DPLATFORM) that overrides the default device tree file. That way projects that want non-standard pinmux configs could bring their own device trees. Cheers, Steve

2 1

seL4 design principles
by Heiser, Gernot (Data61, Kensington NSW) 14 Mar '20

14 Mar '20

I’ve just posted a blog that tries to explain why de do things the way we de in seL4, and why we don’t do some other things, such as hardware abstraction. I hope this helps people understand better which kind of kernel changes are acceptable and which aren’t, and why the API isn’t designed for ease of use. https://microkerneldude.wordpress.com/2020/03/11/sel4-design-principles/ Gernot

3 4

intel-vtd.c::vtd_get_n_paging looks so suspicious
by laokz 14 Mar '20

14 Mar '20

Hello all, kernel/src/plat/pc99/machine/intel-vtd.c::vtd_get_n_paging() confused me a lot. Wish to get any help. This func intends to calculate paging pages needed for all RMRRs. The following code 'filter the identical regions by pci bus id', and use them to figure out the final result. ``` for (word_t i = 1; i < rmrr_list->num; i++) { if (vtd_get_root_index(rmrr_list->entries[i].device) != vtd_get_root_index(filtered.entries[filtered.num - 1].device) && rmrr_list->entries[i].base != filtered.entries[filtered.num - 1].base && rmrr_list->entries[i].limit != filtered.entries[filtered.num - 1].limit) { filtered.entries[filtered.num] = rmrr_list->entries[i]; filtered.num++; } } ``` But vtd_map_reserved_page() says, every different devices(with diff bus-dev- func ID) have their own paging structures. Then why do filter here like this , yet the logic looks so confusing. And on line 313, it counts pages according to the specified level address bits. ``` size += get_n_paging(region, 32 - (VTD_PT_INDEX_BITS * i + seL4_PageBits)); ``` So what does 32 mean? Maybe a typo? Thanks, laokz

2 2

Using sel4.xml/sel4arch.xml to generate custom bindings
by Alexandre Mutel 12 Mar '20

12 Mar '20

Hello, I would like to use the sel4.xml API description files to generate custom bindings for a prototype language to interact directly with seL4 without going through libsel4 C API. I assume that the structure of these files could change, which I'm willing to accept, but wanted to know if these files are here to stay in the future? I understand also that I will still have to parse libsel4 C headers to recover the full API which I'm fine with too. Do you see any trouble following this approach or would you recommend something else?

2 1

May be an error in "alloc_free_io_port_range" of projects/seL4_projects_libs/libsel4vmmplatsupport/src/ioports.c
by yadong.li 12 Mar '20

12 Mar '20

Hi: background: I run virtio_net and virt_con in the lastest version, it is run OK, but I try to add another virito blk, I meet run error below: "Unhandled offset of 0x400 of size 4, reading Assertion failed: !"panic" (/home/yadong.li/seL4_vm_11/sel4_horizon/camkes-arm-vm/projects/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_in: 71)" I add print on my enviornmen, found: ********************start[0x1000], end[0x1400] /*net*/ ********************start[0x1400], end[0x1800] /*con*/ ********************start[0x1800], end[0x1c00] /*blk*/ ---------------------------virtio_con_io_in, con = 0x55f3238, offset = 0x400[0x1800:0x1400] port_no:1800 should belong "blk", but it recongnize as belong "con"(con may be not use the offset 0 feature), the boundary may be have some problem the function: static int alloc_free_io_port_range(vmm_io_port_list_t *io_list, ioport_range_t *io_range) { uint16_t free_port_addr = io_list->alloc_addr; if (free_port_addr + io_range->size < free_port_addr) { /* Possible overflow */ return -1; } io_list->alloc_addr += io_range->size; io_range->start = free_port_addr; io_range->end = free_port_addr + io_range->size; return 0; } I think "io_range->end = free_port_addr + io_range->size;" should change to "io_range->end = free_port_addr + io_range->size - 1;" ? Thank you very much!

2 1

Booting on a Jetson TK1 board.
by Travis Wheatley 11 Mar '20

11 Mar '20

Hello all, I am spinning up on sel4 and having difficulty booting a kernel on a Jetson TK1 board. I have successfully downloaded the cmakes repo and can build the x86 version of the code and run it as a simulation. I can also successfully build the TK1 version by changing the -DARCHETECTURE argument passed to init-build.sh to “tk1”. This results in a single image file named “capdl-loader-image-arm-tk1” to show up in my images folder (as opposed to both a kernel image and “userland” image that get created in the x86 version). So… I put that image on an SD card, plug it into the TK1, boot to a uboot prompt, and load the image using the command “fatload mmc 1 0x82000000 <filename>”. I can use “md” to see that the image is actually loaded properly. However, when I type “go 0x82000000” I see no output what so ever going out of the serial port. What I expect to see is similar output to what was displayed in the x86 simulation. I posted the question to the IRC channel yesterday and someone suggested using bootm or bootelf. No luck with either of these. So… hoping someone here might be able to give me a clue. — Travis

2 4

L4 Risc-v touchscreen board
by Luca Tapponi 27 Feb '20

27 Feb '20

I am newby in this sector and involved in a project to create a prototype (hardware and software) based on risc-v cpu and running L4-based microkernel. I need to control and program an attached touchscreen where I can create a simple graphic user interface too. I would appreciate any suggestion that bring me on the right road. Board should embed wi-fi network too. First step is to find the right hardware and second is to have development tools/environment to program the board. As much as possible open licensing should be adopted because the project falls in IT security solution and want to avoid any hidden backdoors. Thank you in advance. Best regards, Luca

1 0

devices.camkes: vm#.untyped_mmios: What does the integer after the addresses in this array represent?
by Turner, Ben 26 Feb '20

26 Feb '20

Hi all, As stated in the question, I'm not certain about how the integer part of the elements in the untyped_mmios array in devices.camkes are derived? E.g. in the TX2 devices.camkes file: vm0.untyped_mmios = [ "0x3886000:12", // GICV Iface. /* The purpose of these untyped regions is to force the untyped * allocator to treat this memory region as reserved so that when we * try to ensure that the VMM is placed into this region in RAM, it * will definitely be available for placement. * * This address pertains to guest-vm@f1000000 in the overlay DTS */ "0xF1000000:24", "0xF2000000:25", "0xF4000000:26", "0xF8000000:24", ]; I recognise that the range of addresses here covers the VM_RAM_SIZE specified, and so the pattern that emerges is: 24 --> 0x01000000 25 --> 0x02000000 26 --> 0x04000000 And so the above would cover the range 0xf1000000 --> 0xf9000000, which is the range of memory specified for the VM. Is this simply a case of the integer representing double the value with each increment. E.g: Integer Int Rep Hex 0 1 0x0000_0001 1 2 0x0000_0002 2 4 0x0000_0004 3 8 0x0000_0008 4 16 0x0000_0010 5 32 0x0000_0020 6 64 0x0000_0040 7 128 0x0000_0080 8 256 0x0000_0100 9 512 0x0000_0200 10 1024 0x0000_0400 11 2048 0x0000_0800 12 4096 0x0000_1000 13 8192 0x0000_2000 14 16384 0x0000_4000 15 32768 0x0000_8000 16 65536 0x0001_0000 17 131072 0x0002_0000 18 262144 0x0004_0000 19 524288 0x0008_0000 20 1E+06 0x0010_0000 21 2E+06 0x0020_0000 22 4E+06 0x0040_0000 23 8E+06 0x0080_0000 24 2E+07 0x0100_0000 25 3E+07 0x0200_0000 26 7E+07 0x0400_0000 27 1E+08 0x0800_0000 28 3E+08 0x1000_0000 29 5E+08 0x2000_0000 30 1E+09 0x4000_0000 31 2E+09 0x8000_0000 Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner(a)roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

3 2

two questions when I add virtio net with virtio_console meanwhile in arm-vm project
by yadong.li 24 Feb '20

24 Feb '20

hi, I had make virtio_console work OK on my environment（armv8）, But I meet two question when I add virtio net with virtio_console meanwhile. Question1: "add_io_port_range@io.c:111 Requested ioport range 0x6200-0x6600" for VIRTIO CON overlaps with existing range 0x6200-0x6600 for VIRTIO PCI NET According to the print above: common_make_virtio_con(virtio_emul_vm, vm->pci, vm->io_port, VIRTIO_IOPORT_START, VIRTIO_IOPORT_SIZE, VIRTIO_INTERRUPT_PIN, VIRTIO_CON_PLAT_INTERRUPT_LINE, backend); common_make_virtio_net(virtio_emul_vm, vm->pci, vm->io_port, VIRTIO_IOPORT_START + 0x1000, VIRTIO_IOPORT_SIZE, VIRTIO_INTERRUPT_PIN, VIRTIO_NET_PLAT_INTERRUPT_LINE, backend); a、above two function，I found they use the same VIRTIO_IOPORT_START， I modify VIRTIO_IOPORT_START of common_make_virtio_net to （VIRTIO_IOPORT_START + 0x1000）, is it OK? b、I also found（VIRTIO_CON_PLAT_INTERRUPT_LINE == VIRTIO_NET_PLAT_INTERRUPT_LINE）,is that OK? Whether it should be make interrupt line different ? Question2: "_utspace_split_alloc@split.c:272 Failed to find any untyped capable of creating an object at address 0xc0001000 Failed to find device cap for 0xc0001000" According to the print above: a、my PCI region define as below: #define PCI_CFG_REGION_ADDR 0xC1000000 #define PCI_IO_REGION_ADDR 0xC0000000 #define PCI_CFG_REGION_SIZE 0x1000000 #define PCI_IO_REGION_SIZE 0x1000 #define PCI_CFG_BAR_MASK 0xFFFFFFFF I found 'virtio_net_init' and 'virtio_console_init' will call the same function 'install_virtio_vpci_device', net and console will have the same PCI_IO_REGION_ADDR ? is it OK? b、If I want to support two or muti virtio device, which should I add a new macro define for virtio_net in a? for example add PCI_IO_REGION_ADDR for net or add PCI_CFG_REGION_ADDR ? c、Can you give me some list file to change for support for support net and console meanwhile? Thank you very much.

2 2

Adding Platform Support: CAmkES-ARM-VM: VM_Minimal: Raspberry Pi 3b
by Turner, Ben 21 Feb '20

21 Feb '20

Hi, I have been attempting to add support for the Raspberry Pi 3 b platform so that I can run the vm_minimal application on it. The platform supports ARM_HYP, so I believe it should be possible to get this working. I have reached to point where ninja errors on an implicit declaration for `set_gic_vcpu_ctrl_hcr`. From what I understand, this is to do with the ARM Generic Interrupt Controller, however the RPi3b doesn't have a GIC, it has a `bcm2836-armctrl-ic`. This occurs because the file vcpu.h defines an inline function that calls this function, however as the RPi3b doesn't have a GIC, neither the gic_v2.h or gic_v3.h files are provided in the build environment, and hence the build fails. I am unsure what this means in terms of implementation. What needs to be added or changed to get this compiling for the RPi3b? Thanks in advance Ben Turner ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

3 9

Announcing new releases: seL4-11.0.0, camkes-3.8.0, CapDL-0.1.0,
by Mcleod, Kent (Data61, Kensington NSW) 20 Feb '20

20 Feb '20

Announcing the releases of seL4, CAmkES, CapDL and updates of other supporting projects. **Note that this announcement refers to a series of release commits that occurred on 19-Nov-2019.** See below for links to release notes. In addition there are new ways to discuss seL4 and trustworthy systems: - seL4 Discourse at <https://sel4.discourse.group>, a forum for attempting to build up an seL4 knowledge base. - seL4 Mattermost at <https://mattermost.ts.data61.csiro.au/sel4-external/> for online messaging. (Signup link can be found on seL4 Discourse:<https://sel4.discourse.group/t/sel4-mattermost-sign-up-link/125> with a valid account). - seL4 RFCs at <https://sel4.atlassian.net/projects/RFC> for open discussion about major changes to the seL4 ecosystem. For more information see: <https://docs.sel4.systems/processes/#contact> Versioned Releases * seL4 11.0.0: The seL4 microkernel <https://docs.sel4.systems/releases/sel4/11.0.0> * CAmkES camkes-3.8.0: Component Architecture for microkernel-based Embedded Systems <https://docs.sel4.systems/releases/camkes/camkes-3.8.0> * CapDL 0.1.0: Collection of tools for generating, parsing and loading CapDL specifications of systems <https://docs.sel4.systems/releases/capdl/0.1.0> Update notes * seL4 Buildsystem: System configuration and building using mostly CMake <https://docs.sel4.systems/updates/buildsystem/11.0.x.html> * seL4Test: Test suite for seL4 <https://docs.sel4.systems/updates/sel4test/11.0.x.html> * sel4bench: sel4bench contains benchmarking applications and a support library for seL4 <https://docs.sel4.systems/updates/sel4bench/11.0.x.html> * user_libs: Userlevel libraries on seL4 <https://docs.sel4.systems/updates/user_libs/11.0.x.html> * The seL4 Run-time: A minimal runtime for running a C or C-compatible process in a minimal seL4 environment <https://docs.sel4.systems/updates/sel4runtime/11.0.x.html> * Elfloader: For preparing the hardware for seL4 on ARM and RISC-V <https://docs.sel4.systems/updates/elfloader/11.0.x.html> * seL4 tutorials: Collection of tutorials for learning to use seL4 and its ecosystem <https://docs.sel4.systems/updates/sel4-tutorials/camkes-3.8.x.html> * camkes-vm: x86 Virtual Machine build as a CAmkES component <https://docs.sel4.systems/updates/camkes-vm/camkes-3.8.x.html> * camkes-arm-vm: Arm Virtual Machine build as a CAmkES component <https://docs.sel4.systems/updates/camkes-arm-vm/camkes-3.8.x.html> * seL4webserver: A reference for implementing applications on seL4 <https://docs.sel4.systems/updates/sel4webserver/camkes-3.8.x.html> An seL4 discourse version of this email can be found at: <https://sel4.discourse.group/t/19-november-2019/126>

1 0

Re: [seL4] Multikernels and resource transfer
by Ge, Qian (Data61, Kensington NSW) 14 Feb '20

14 Feb '20

In a multikernel setup, each kernel manages its own memory allocation, as the main memory is distributed among all valid kernels. Hence, the described scenario does not apply. Regards, Qian. Message: 1 Date: Thu, 13 Feb 2020 00:49:11 -0500 From: Demi Obenour <demiobenour(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] Multikernels and resource transfer Message-ID: <CAJEMUN_L49O9btYx03Z35uQ6S21T80wPujP86Gd5XyymH4BQ6g(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" In a multikernel, how would retyping work? Obviously, the kernel cannot allow untyped X to be used for page tables if user code on another core might still have write access to it. Would retyping involve some sort of in-kernel concurrency? Obviously, the clustered multikernel avoids this, but making applications (as opposed to low-level libraries and services) work around kernel limitations seems rather unappealing. Sincerely, Demi

1 0

Multikernels and resource transfer
by Demi Obenour 13 Feb '20

13 Feb '20

In a multikernel, how would retyping work? Obviously, the kernel cannot allow untyped X to be used for page tables if user code on another core might still have write access to it. Would retyping involve some sort of in-kernel concurrency? Obviously, the clustered multikernel avoids this, but making applications (as opposed to low-level libraries and services) work around kernel limitations seems rather unappealing. Sincerely, Demi

1 0

Beginner ARM_HYP questions
by tossel＠gmail.com 11 Feb '20

11 Feb '20

Greetings, I'm trying to understand how hypervisor functionality support is working in seL4 for aarch32/aarch64. In the documentation there is a list of platforms [1] for some of them ARM_HYP is said to be supported for some not. I was trying to grep through the kernel, but it seemed to me that ARM_HYP can be enabled on any ARM-based platform. I've tried to compile sel4test for exynos5422 (for which ARM_HYP is said to be enabled) and odroidc2 (for which it is said that it's not supported) with -DARM_HYP=ON manually set, and for both compilation succeeded. It failed for hikey, that should support it, but that's a different story. So my questions are - How is it defined whether ARM_HYP is supported for a board/SoC, provided that processor architecture supports it? What the platform support code should provide for hypervisor to work? - For platforms not supported by camkes-arm-vm (like, most of the platforms) how ARM_HYP can be tested? Thanks a lot, Anton Gerasimov [1] https://docs.sel4.systems/Hardware/

2 2

(no subject)
by abdi mahmud haji 11 Feb '20

11 Feb '20

hello can someone help me here what did i do wrong ,i have been trying to do camkes-vm-linux and i have followed the instruction on sel4-tutorials when i run ninja to build the file i have got an error as below ========================================================================== ninja [5/127] Building C object camkes-vm-li...ents/Init/src/virtio_net_vswitch.c.obj FAILED: ccache /usr/bin/gcc --sysroot=/home/sel4/sel4-tutorials-manifest/camkes-vm-linux_build -I../projects/camkes/vm/components/Init/src -I../projects/camkes/vm/components/VM/configurations -Icamkes-vm-linux/vm0/include -I../kernel/libsel4/include -I../kernel/libsel4/arch_include/x86 -I../kernel/libsel4/sel4_arch_include/x86_64 -I../kernel/libsel4/sel4_plat_include/pc99 -I../kernel/libsel4/mode_include/64 -Ilibsel4/include -Ilibsel4/arch_include/x86 -Ilibsel4/sel4_arch_include/x86_64 -I../projects/sel4runtime/include -I../projects/sel4runtime/include/mode/64 -I../projects/sel4runtime/include/arch/x86 -I../projects/sel4runtime/include/sel4_arch/x86_64 -Iprojects/musllibc/build-temp/stage/include -Ilibsel4/autoconf -Ikernel/gen_config -Ilibsel4/gen_config -I../tools/camkes/libsel4camkes/include -I../projects/seL4_libs/libsel4debug/include -I../projects/seL4_libs/libsel4debug/arch_include/x86 -I../projects/seL4_libs/libsel4debug/sel4_arch_include/x86_64 -I../projects/util_libs/libutils/include -I../projects/util_libs/libutils/arch_include/x86 -Iprojects/util_libs/libutils/gen_config -I../projects/util_libs/libplatsupport/include -I../projects/util_libs/libplatsupport/plat_include/pc99 -I../projects/util_libs/libplatsupport/arch_include/x86 -Iprojects/util_libs/libplatsupport/gen_config -I../projects/seL4_libs/libsel4muslcsys/include -I../projects/util_libs/libcpio/include -I../projects/seL4_libs/libsel4utils/include -I../projects/seL4_libs/libsel4utils/sel4_arch_include/x86_64 -I../projects/seL4_libs/libsel4utils/arch_include/x86 -I../projects/seL4_libs/libsel4vspace/include -I../projects/seL4_libs/libsel4vspace/arch_include/x86 -I../projects/seL4_libs/libsel4vka/include -I../projects/seL4_libs/libsel4vka/sel4_arch_include/x86_64 -I../projects/seL4_libs/libsel4vka/arch_include/x86 -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -I../projects/seL4_libs/libsel4simple/include -I../projects/seL4_libs/libsel4simple/arch_include/x86 -I../projects/seL4_libs/libsel4platsupport/include -I../projects/seL4_libs/libsel4platsupport/arch_include/x86 -I../projects/seL4_libs/libsel4platsupport/plat_include/pc99 -I../projects/seL4_libs/libsel4simple-default/include -I../projects/util_libs/libelf/include -Iprojects/seL4_libs/libsel4muslcsys/gen_config -I../projects/seL4_libs/libsel4sync/include -I../projects/projects_libs/libvirtqueue/include -Icamkes-vm-linux/libsel4camkes/gen_config -Iprojects/sel4runtime/gen_config -I../projects/seL4_libs/libsel4allocman/include -I../projects/seL4_libs/libsel4allocman/sel4_arch/x86_64 -I../projects/seL4_libs/libsel4allocman/arch/x86 -I../projects/seL4_libs/libsel4vmm/include -I../projects/util_libs/libpci/include -I../projects/util_libs/libethdrivers/include -I../projects/util_libs/libethdrivers/plat_include/pc99 -I../projects/util_libs/libethdrivers/arch_include/x86 -Iprojects/util_libs/libethdrivers/gen_config -Iprojects/util_libs/liblwip/gen_config -Iprojects/util_libs/libpicotcp/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Icamkes-vm-linux/vm/gen_config -I../projects/projects_libs/libvswitch/include -I../projects/camkes/global-components/components/FileServer/libFileServer-client/. -m64 -march=nehalem -D__KERNEL_64__ -g -nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mtls-direct-seg-refs -Wno-main -std=gnu11 -MD -MT camkes-vm-linux/CMakeFiles/vm0.instance.bin.dir/__/projects/camkes/vm/components/Init/src/virtio_net_vswitch.c.obj -MF camkes-vm-linux/CMakeFiles/vm0.instance.bin.dir/__/projects/camkes/vm/components/Init/src/virtio_net_vswitch.c.obj.d -o camkes-vm-linux/CMakeFiles/vm0.instance.bin.dir/__/projects/camkes/vm/components/Init/src/virtio_net_vswitch.c.obj -c ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘virtio_net_notify_vswitch_send’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:50:23: warning: implicit declaration of function ‘virtqueue_driver_dequeue’ [-Wimplicit-function-declaration] int dequeue_res = virtqueue_driver_dequeue(node->virtqueues.send_queue, ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘emul_raw_tx’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:123:13: error: unknown type name ‘virtqueue_t’ virtqueue_t *destbuff; ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:147:19: warning: implicit declaration of function ‘virtqueue_driver_enqueue’ [-Wimplicit-function-declaration] err = virtqueue_driver_enqueue(destnode->virtqueues.send_queue, ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:157:19: warning: implicit declaration of function ‘virtqueue_driver_signal’ [-Wimplicit-function-declaration] err = virtqueue_driver_signal(destnode->virtqueues.send_queue); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:170:17: warning: implicit declaration of function ‘virtqueue_driver_poll’ [-Wimplicit-function-declaration] if (virtqueue_driver_poll(destnode->virtqueues.send_queue) == 1) { ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘virtio_net_notify_vswitch_recv’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:215:5: error: unknown type name ‘virtqueue_t’ virtqueue_t *rxdata_buff; ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:234:23: warning: implicit declaration of function ‘virtqueue_device_dequeue’ [-Wimplicit-function-declaration] int dequeue_res = virtqueue_device_dequeue(node->virtqueues.recv_queue, ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:249:27: warning: implicit declaration of function ‘virtqueue_device_enqueue’ [-Wimplicit-function-declaration] enqueue_res = virtqueue_device_enqueue(node->virtqueues.recv_queue, available_buff, available_buff_sz); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:275:11: warning: implicit declaration of function ‘virtqueue_device_signal’ [-Wimplicit-function-declaration] err = virtqueue_device_signal(node->virtqueues.recv_queue); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘virtio_net_notify_vswitch’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:292:17: warning: implicit declaration of function ‘virtqueue_device_poll’ [-Wimplicit-function-declaration] if (virtqueue_device_poll(g_vswitch.nodes[i].virtqueues.recv_queue) == 1) { ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘make_vswitch_net’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:312:44: warning: passing argument 1 of ‘camkes_virtqueue_driver_init’ from incompatible pointer type [-Wincompatible-pointer-types] err = camkes_virtqueue_driver_init(&send_virtqueue, mac_mapping.send_id); ^ In file included from ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:29:0: ../tools/camkes/libsel4camkes/include/camkes/virtqueue.h:64:5: note: expected ‘virtqueue_driver_t * {aka struct virtqueue_driver *}’ but argument is of type ‘virtqueue_driver_t ** {aka struct virtqueue_driver **}’ int camkes_virtqueue_driver_init(virtqueue_driver_t *driver, unsigned int camkes_virtqueue_id); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:317:44: warning: passing argument 1 of ‘camkes_virtqueue_device_init’ from incompatible pointer type [-Wincompatible-pointer-types] err = camkes_virtqueue_device_init(&recv_virtqueue, mac_mapping.recv_id); ^ In file included from ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:29:0: ../tools/camkes/libsel4camkes/include/camkes/virtqueue.h:72:5: note: expected ‘virtqueue_device_t * {aka struct virtqueue_device *}’ but argument is of type ‘virtqueue_device_t ** {aka struct virtqueue_device **}’ int camkes_virtqueue_device_init(virtqueue_device_t *device, unsigned int camkes_virtqueue_id); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:320:13: warning: implicit declaration of function ‘camkes_virtqueue_driver_free’ [-Wimplicit-function-declaration] camkes_virtqueue_driver_free(send_virtqueue); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:333:13: warning: implicit declaration of function ‘camkes_virtqueue_device_free’ [-Wimplicit-function-declaration] camkes_virtqueue_device_free(recv_virtqueue); ^ [5/127] Building C object camkes-vm-li...MakeFiles/sel4camkes.dir/src/dma.c.obj ninja: build stopped: subcommand failed. ================================================================== and why this happing

2 1

Problem booting camkes arm vmm on TK1 from SD Card
by Mike Clark 10 Feb '20

10 Feb '20

I'm using the docker image to build the CAmkES ARM VMM project using roughly the instructions here: https://docs.sel4.systems/VM/CAmkESARMVM.html (they are slightly out of date). I do: ../init-build.sh -DAARCH32=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tk1 ninja Then I copy the resulting image from the images directory to an SD card and put that in my TK1. When U-Boot starts I use the following commands to try to boot fatload mmc 1 0x10000000 capdl-loader-image-arm-tk1 bootelf 0x10000000 To which I get an error: No elf image at address 0x10000000 I tried with an older version of U-Boot (that worked following this same procedure about a year ago). It is U-Boot SPL 2014.10-rc2-g3127911 (Jun 07 2016 - 21:00:01) I also tried updating U-Boot to U-Boot SPL 2020.01-00442-gc00bd81ae0 (Jan 10 2020 - 11:10:18 -0500). Same error. Any thoughts or suggestions on how I get this to boot?

4 14

GPIO on Sabre imx6
by Parvaneh Ahgajani 10 Feb '20

10 Feb '20

Hello all, I am working with sabre lite board and using camkes framework. In my implementation I have a driver component that has 7 dataport buf and I connected these buffers to hardware component. In source of component driver I am initialize gpio_sys, mux_sys and pins using these functions: - imx6_mux_init() - imx6_gpio_sys_init() - gpio_new() Here I have copied some part of my code: ****************************************** gpio_sys_t gpio_sys; gpio_t pins[32*7]; mux_sys_t mux_sys; void gpio__init() { imx6_mux_init(NULL, &mux_sys); imx6_gpio_sys_init((void*)gpio0, (void*)gpio1, (void*)gpio2, (void*)gpio3, (void*)gpio4, (void*)gpio5, (void*)gpio6, &mux_sys, &gpio_sys); } void gpio_init_pin(int pin, int direction) { if(pin>0 && pin< sizeof(pins)/sizeof(pins[0])) { gpio_new(&gpio_sys, pin, (enum gpio_dir)direction, &pins[pin]); } } void gpio_set_pin(int pin, int value) { if(pin >= 0 && pin < (sizeof(pins)/sizeof(pins[0]))) { if(value) { gpio_set(&pins[pin]); } else { gpio_clr(&pins[pin]); } } } int gpio_read_pin(int pin) { if(pin>0 && pin< sizeof(pins)/sizeof(pins[0])) { return gpio_get(&pins[pin]); } return -1; } ****************************************** By calling "gpio_init_pin(ALARM_PIN= 28, 0);" I am getting this error: Assertion failed: bank->data == v (PATH/projects/util_libs/libplatsupport/src/plat/imx6/gpio.c: imx6_gpio_write: 144) How can I fix this error? How should I specify the GPIO pins? Thank you for your time and consideration, Parvaneh.

2 3

(no subject)
by abdi mahmud haji 06 Feb '20

06 Feb '20

hi everybody i have quick questions regarding how can you take an input form terminal in seL4,i am trying to run a simple code of my own on sel4 and to display a message we use printf(), why scanf() is not working for me the way printf work.is there another way to do that

2 1

Question about MCS branch
by Isaac Beckett 05 Feb '20

05 Feb '20

I have a bit of a noobish question, why are timing/scheduling abilities being added to the kernel? I understand that userland still controls scheduling, regardless of which branch is being used, but I'm confused as to wby scheduling features needed to be added to the kernel itself.

2 1

Configuring CAmkES projects
by Grant Jurgensen 01 Feb '20

01 Feb '20

Hi everyone, I have a couple questions regarding the current CMake build structure for CAmkES projects. It seems that the current structure intends you to put your project in the camkes/apps folder, and then build your project with `../init-build -DCAMKES_APP=<project_name>`, or the equivalent using the griddle script. What I don't understand is how you are supposed to configure your project. It seems easy_settings.cmake is always loaded. Is it advisable to edit this file? In the past, I could also tweak configuration variables manually by invoking the ccmake gui on the top-level directory. Now that there is no CMakeLists.txt in the top-level directory, this does not work. If I try it in my project's directory, it tells me the cache is empty. Is it still possible to edit CMake cache variables with ccmake? Thanks! Grant Jurgensen

2 2

Recycle resources used by a thread after it terminates
by Alexandre Mutel 01 Feb '20

01 Feb '20

Hi, I have a design question regarding how to recycle capabilities/memory frames that were used by a thread once it terminates. Let's assume that there is a MemoryManager server responsible to serve virtual memory to user processes (e.g similar to implementing VirtualAlloc). The MemoryManager has to maintain the list of untyped object, retype them, maintain likely a list of resources allocated for a user thread, likely copy/mint the page frames to forward them to the user process...etc. But when a thread terminates, as I can't see any related events in seL4, I would assume that the user process would have to explicitly notify the MemoryManager on exit. Then the MemoryManager would know which user thread has exited and would update/recover the used capabilities and destroy them, in order to recover untyped objects. Would it be a proper design that plays well with seL4? Do you think that it could be done more efficiently with seL4? Thank you!

2 2

AMD CPUs and SMP scalability
by Demi M. Obenour 30 Jan '20

30 Jan '20

My understanding is that seL4 plans on scaling to large multi-core server processors by using Intel TSX. However, AMD has not implemented TSX, and TSX has been involved in many recent side-channel attacks. AMD systems are attractive both from a performance and a security perspective, but my understanding is that the performance of seL4 on them will be terrible. Are there plans to implement and verify a version of seL4 that scales to multicore AMD server-class CPUs? The problem with a multikernel is that not having thread migration is likely to cause starvation on many practical workloads Sincerely, Demi

2 2

Status of side-channel attack mitigation
by Demi M. Obenour 30 Jan '20

30 Jan '20

What is the current status of seL4 with respect to Meltdown, Spectre, L1TF, MDS and other CPU vulnerabilities? Thank you, Demi

2 2

(no subject)
by abdi mahmud haji 29 Jan '20

29 Jan '20

hi i have been wondering how can i install or put another OS( like , window ,linux )on the top of seL4 microkernel can some one help

2 1

Are there any plans to re-add seL4_Untyped_RetypeAtOffset?
by Andrew Warkentin 29 Jan '20

29 Jan '20

Speaking of things that would be useful for large dynamic systems, are there any plans to add seL4_Untyped_RetypeAtOffset from the old experimental branch to the current mainline kernel? I am writing a buddy untyped allocator for UX/RT, and being able to retype at arbitrary offsets would reduce overhead quite a bit because I could just retype from the highest-order untyped objects most of the time rather than having to create two child untyped objects per split. If not, I will probably end up re-adding it myself later on (sometime after UX/RT is running actual user programs).

5 20

Camkes and Memory-Mapped Peripherals
by Michael Neises 29 Jan '20

29 Jan '20

Hello, I'm trying to access a memory-mapped peripheral on the exynos5422 (ODROID XU4). I have the physical address of the peripheral's registers from the exynos5422 data sheet. As per the Camkes manual, I've used the seL4HardwareMMIO connection type to facilitate this. However, while I can use the excess bytes of the "dataport Buf" as expected, there is a data fault when I try to read from the peripheral's memory-mapped (and readable) registers: """ FAULT HANDLER: data fault from test_component.test_component_0_control (ID 0x1) on address 0, pc = 0x3250c, fsr = 0x211 """ Besides defining the hardware component and this connection in Camkes, is there anything else I must do? I will appreciate any guidance on this matter. Best, Michael Neises

2 1

Re: [seL4] Request for enhancement: Notification queues
by Millar, Curtis (Data61, Kensington NSW) 24 Jan '20

24 Jan '20

> I strongly suspect the more fundamental and general extension would be > to remove the scalability limitation of Notifications, probably by > generalising them to a hierarchy, i.e. you signal a sub-notification > which then signals the higher-level notification. I?m not claiming > having thought this through, though. Having thought about this a little, I think that it is useful to observe that the case where such cases where large numbers of notifications need to be received the receiver uses a roughly similar interface to endpoints (seL4_Send to wait for an event and seL4_NBSend to poll for events). If we allow send queues of endpoints to include notification objects in addition to threads we could multiplex notifications via an endpoint by binding the notifications to the endpoint. This could also allow for the removal of notification binding for threads; if they want to receive both notifications and synchronous IPC they can bind the notification to the endpoint. This design should also work with MCS whereby donation of scheduling contexts from notification objects would become roughly the same as donation from a thread with a scheduling context. I think the cleanest implementation would be to allow a notification to contain its own endpoint capability, similar to the manner in which TCBs conatain capabilities. Any time an idle notification is invoked with a send it then queues on the endpoint to which is capability refers if one exists. Send invocations of 'active' (potentially queued) notifications would perform the same XOR operation as currently occurs. When receiving on an endpoint where the first blocked object is a notification the badge received is the badge of the endpoint capability owned by the notification and the notification word is simply placed in the first message register. Whilst I think that this (or something similar) is the most simple case for implementing multiplexing it would have some impact on the semantics and implementation of some objects. Even at this small a scale the verification burden will still be considerable as this change would impact all verified builds. I think further discussion and evaluation of a solution is needed before we can determine that it is sufficiently beneficial to have this feature in the kernel and to commit to maintaining the feature and including it in the verified configurations. Cheers, Curtis Millar

2 1

Request for enhancement: Notification queues
by Demi M. Obenour 23 Jan '20

23 Jan '20

While studying seL4, I noticed that there is no mechanism to wait for one of many notifications. This proposal solves this with a new type of capability, which I call a notification queue. I don’t have the knowledge to determine how they should be implemented, so instead I will describe the general idea. A notification queue is a capability to which notification objects can be attached. When an attached endpoint is notified, a user-provided pointer is pushed onto the queue. Notification queues are edge-triggered, so subsequent notifications do not cause further entries to be added to the queue unless the notification has been read. The queue is implemented as a buffer which is read-only to userspace, but read-write to seL4. When creating a notification queue, userspace must provide sufficient untyped memory to ensure that the queue will not fill up. This ensures that sending a notification cannot fail due to resource exhaustion. Queues can be resized by the application if needed. Attempts to add too many endpoints to a queue results in an error being returned. A notification object can only be attached to one notification queue at a time. It can be detached from a queue and later attached to another. Notification queues can be used whenever a notification object is expected, except that they cannot be badged. Badging a notification queue would make no sense. When polled, a notification queue returns the number of events that have been added to it since it was last polled. Adding one notification queue to another may or may not be allowed. Allowing it would increase flexibility, but also increase implementation complexity. It is also possible to attach a TCB to a queue; the queue is notified when the TCB exits. Only seL4 can send to a notification queue. No userspace process can ever possess a send capability to such a queue. While a notification queue can be accessed from any number of tasks, performance on multi-core systems may be improved if each queue is used from the same core that its attached notifications are used on. Constructive feedback on this proposal is welcome. Sincerely, Demi

3 8

seL4 on unverified ARM platforms
by Demi M. Obenour 23 Jan '20

23 Jan '20

My understanding is that seL4 is currently only verified for one particular ARM platform. Is it considered production-ready on other ARM boards? Sincerely, Demi

2 3

Re: [seL4] Request for enhancement: Notification queues
by Heiser, Gernot (Data61, Kensington NSW) 23 Jan '20

23 Jan '20

On 22 Jan 2020, at 14:44, Demi Obenour <demiobenour(a)gmail.com<mailto:demiobenour@gmail.com>> wrote: But everything needs a really convincing argument, that’s based on a functional limitation that prevents implementation of certain important classes of systems. If it’s only a performance argument, we’ll need to be convinced that it really is a performance bottleneck in realistic systems. Do you believe it is likely to be? I haven’t seen a convincing use case where it is. Gernot

1 0

Plans for verification of IOMMU support on x86? Binary verification?
by Demi M. Obenour 21 Jan '20

21 Jan '20

Are there plans to verify the IOMMU support on x86? x86 without DMA is not very useful, so IOMMU support is needed for the proofs to apply in practice. Sincerely, Demi

2 1

Initializing of the sel4 tutorials fails because of missing the CMakeLists.txt
by Florian Berenbrinker 16 Jan '20

16 Jan '20

2 3

Re: [seL4] Suggestion for Abdurahman
by Harry Butterworth 11 Jan '20

11 Jan '20

Take a look at Andy’s Binary Editor nyangau.org/be/be.html and implement an open source equivalent as an integrated debugger for seL4. You will need to be able to get keyboard input, write characters to the screen and get access to files containing the structure definitions. You can provide the structure definitions at boot time. You won’t need an OS or POSIX or even much of a standard library; the implementation just requires the language runtime, a parser, a few data structures, and a bit of printf-like code. You could write it all and make it completely self-contained which would allow you to keep the footprint really small. Steps to proceed are as follows: 1) Pick a language. I’d probably pick C++ for this but you might also consider D or Rust or maybe COGENT. 2) Work out how to write a small test program in your chosen language and get seL4 to run it. This will require an implementation of the runtime for the language. If this hasn’t been done already for the language you pick, you can implement bits of the runtime as you go along when they are needed. If you fail at this step, go back to step 1, pick a different language. 3) Work out how to get your test program to write characters to the screen (or serial console perhaps). 4) Work out how to get keyboard input. 5) Define the grammar for the structure definitions. If you happen to pick COGENT you might look at DARGENT. 6) Understand the Model View Controller design pattern. 7) Write a parser to parse the structure definitions to create a model. You’ll want the model to use lazy evaluation so the whole system defined by the structure definitions can be represented but there is only overhead for the bits that are being actively browsed. 8) Implement a view for the model which displays a selected part on the console. 9) Implement a controller for the view and model which is an event loop that handles keyboard input and manipulates the model and view accordingly. After getting your new debugger to work for browsing the entire system including the kernel data structures, find a way to integrate it which allows it to be configured to run with only the capability it needs for the debugging you want to do. After that you could make sure it can be used for debugging real time applications with a guarantee not to interfere with their real time operation. For bonus points, if you have picked COGENT, you might finish off with a formal proof that your debugger displays the correct characters on the console according to the structure definitions, contents of memory and history of keyboard input. This (in fact the whole task) would be complicated by the fact that the memory contents change all the time underneath you as you browse a live system so you’d have to work out how to incorporate that and still prove something useful. Enjoy On Fri, Jan 10, 2020 at 8:21 PM abdi mahmud haji < abdimahmudhaji227(a)gmail.com> wrote: > hey guys > I'm abdurahman and i have same question for you > i have been studying microkernel for a little well now specially seL4 and > i have done almost every tutorials in sel4 -tutorials and i have a crazy > idea ,that is i when try to build a 'shell or prompt' on the seL4 > mircokernel but i don't have any idea how to do or where to start . does > any one have a suggestion for me > > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel >

1 1

(no subject)
by abdi mahmud haji 11 Jan '20

11 Jan '20

hey guys I'm abdurahman and i have same question for you i have been studying microkernel for a little well now specially seL4 and i have done almost every tutorials in sel4 -tutorials and i have a crazy idea ,that is i when try to build a 'shell or prompt' on the seL4 mircokernel but i don't have any idea how to do or where to start . does any one have a suggestion for me

4 3

Using seL4_DebugSnapshot()
by rasd＠riseup.net 09 Jan '20

09 Jan '20

Can someone provide more information about using seL4_DebugSnapshot? >From its description in documentation, I would expect it to print out a CapDL struct over a debugging port/console. Instead, it waits for user commands for various data types sends back binary data[0]. Since the commands are all 0xa0-0xff[1], it doesn't seem like DebugSnapshot expects a human and a keyboard to be present on the other end. Is there some internal debugging tool that is supposed to be used with this system call? Is DebugSnapshot still used? Any advice or information is appreciated. ras [0] https://github.com/seL4/seL4/blob/master/src/arch/arm/32/machine/capdl.c [1] https://github.com/seL4/seL4/blob/master/include/machine/capdl.h

2 1

答复: some question about the compile of global-components in camkes_arm_vm project
by yadong.li 09 Jan '20

09 Jan '20

I found some example in odroid_vm, I want to make sure my understanding is correct? In CMakeLists.txt DeclareCAmkESComponent(HelloWorld) is just tell me there is a component called “HelloWorld” If you want this component to be compiled to project You must add call in your assembly in .cmakes file like below: assembly { composition { component HelloWorld hello; } Thank you very much 发件人: yadong.li 发送时间: 2019年12月28日 15:32 收件人: 'devel(a)sel4.systems' 主题: some question about the compile of global-components in camkes_arm_vm project hi， I have some question about the compile of global-components in camkes_arm_vm project. 1、In projects/global-components/components, there are some directory include FileServer, SerialServer, TimeServer and the others. I found FileServer had been compiled to project， but the other directory have not been compiled Is there some on-off switch control the compile ？ But I did not find it. 2、The CAmkES of FileServer component did not have a "int run(void) {}, If I want to add an new component with run entry， but it is not rootserver（I think one project only have one rootserver），it run with vm rootserver parallelly？ what should I do ？ Is there some example. Thank you very much

2 1

Error while building in docker
by Edward Sandberg 09 Jan '20

09 Jan '20

This morning I saw this error when building sel4: /bin/sh: 1: PROTOBUF_PROTOC_EXECUTABLE-NOTFOUND: not found I noticed a warning when starting the docker container about trustworthysystems/camkes:latest being over 30 days old. I thought that using an up to date pull of: https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git would keep the build env up to date but that apparently is either not the case or there is a problem with the repo. I ran: docker pull trustworthysystems/camkes and the warning was resolved and I could build seL4. Is pulling that docker image supposed to be necessary? Thanks! -- Edward Sandberg Adventium Labs 111 3rd Avenue S. Suite #100 Minneapolis, MN 55401 ed.sandberg(a)adventiumlabs.com

2 1

fastpath performance test
by Dd Nirvana 05 Jan '20

05 Jan '20

Hi guys, I have downloaded the lastest seL4 repo and built the seL4 kernel. And I reuse the code in sel4test/projects/sel4test/apps/sel4test-tests/src/tests/ipc.c. To test the fast, I made minor modifications: first, set caller and callee to the same priority; second, caller uses seL4_Call while callee uses seL4_ReplyRecv. However, the fastpath takes more than 2000 cycles (a round trip). Build: use the lastest provided docker and ../init-build.sh - DPLATFORM=x86_64 -DCMAKE_BUILD_TYPE=Release Both hardware and Qemu show similar results. (4.0GHz skylake CPU) BTW. The manifest is the same as https://sel4.systems/About/Performance/home.pml (i.e., bf13e9f673484825a60f9950cf688ff33ac841ad). Any advices about the issue? Best, Jinyu Gu, Institute of Parallel and Distributed Systems (IPADS), School of Software, Shanghai Jiao Tong University

2 1

Understand seL4 x86_64 Kernel ABI calling convention
by Alexandre Mutel 03 Jan '20

03 Jan '20

Hello! While looking at the code base and checking generated code, I'm not sure about the pertinence of having a different ABI from user System V ABI for kernel calls, as it is implying a bit more unnecessary register shuffling, and I was wondering why this choice was made to have r10, r8, r9, r15? instead of keeping System V ABI and just replace rcx by r10 as it is discarded by syscall: SystemVABI_x86_64_user: rdi, rsi, rdx, rcx, r8, r9 SystemVABI_x86_64_Linux_kernel: rdi, rsi, rdx, r10, r8, r9 SystemVABI_x86_64_seL4: rdi, rsi, r10, r8, r9, r15 So on a Linux Kernel, only the register rcx will be transferred to r10 (when transitioning from user to syscall), but in seL4, it has to reshuffle arguments rdx to r9. (Note for context: I'm working on a project where I don't use a standard C compiler to interface with the seL4 Kernel API, and where the register allocator of the compiler might not be as efficient as GCC/CLang after everything is inlined, that's why I'm looking into these details)

1 1

Hardware-aided Trusted Computing devroom at FOSDEM
by Vasily A. Sartakov 31 Dec '19

31 Dec '19

Hello I would like to invite your to participate in a new devroom: Hardware-aided Trusted Computing. The devroom is devoted to open source projects on top of modern TEEs like Intel SGX, AMD SEV/SVE, Arm TrustZone. You can find the schedule here: https://fosdem.org/2020/schedule/track/hardware_aided_trusted_computing/ I hope this will be interesting for the community. See you at FOSDEM. -- Dr.-Eng. V. A. Sartakov

2 1

some question about the compile of global-components in camkes_arm_vm project
by yadong.li 28 Dec '19

28 Dec '19

hi， I have some question about the compile of global-components in camkes_arm_vm project. 1、In projects/global-components/components, there are some directory include FileServer, SerialServer, TimeServer and the others. I found FileServer had been compiled to project， but the other directory have not been compiled Is there some on-off switch control the compile ？ But I did not find it. 2、The CAmkES of FileServer component did not have a "int run(void) {}, If I want to add an new component with run entry， but it is not rootserver（I think one project only have one rootserver），it run with vm rootserver parallelly？ what should I do ？ Is there some example. Thank you very much

1 0

Camkes Project on Sabre Lite i.mx6 board
by Parvaneh Ahgajani 19 Dec '19

19 Dec '19

Hello all, I am trying to have my own seL4 demo on Sabre Lite board. I am using this command to create the image file: ../init-build.sh -DPLATFORM=sabre -DCROSS_COMPILER_PREFIX=arm-linux-gnueabi- -DCAMKES_APP=adder After that I run this commands to boot the image: fatload mmc 1 0x41000000 adder(image file) The bootm command gives this error: Wrong Image Format for bootm command ERROR: can't get kernel image! I tried bootelf but it stuck and does not show the correct answer: bootelf 0x41000000 CACHE: Misaligned operation at range [10598000, 105980a4] CACHE: Misaligned operation at range [10599000, 105a3434] CACHE: Misaligned operation at range [105a3434, 105a3c23] CACHE: Misaligned operation at range [107fc000, 1080a038] ## Starting application at 0x10598000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[10598000..1080a037] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 1069c064. Loaded DTB from 1069c064. paddr=[10038000..10042fff] ELF-loading image 'kernel' paddr=[10000000..10037fff] vaddr=[e0000000..e0037fff] virt_entry=e0000000 ELF-loading image 'capdl-loader' paddr=[10043000..1019bfff] vaddr=[10000..168fff] virt_entry=188dc ELF loader relocated, continuing boot... Enabling MMU and paging It seems It does not go to kernel-image entry point and bootstrap the kernel! Is there any thing that I need to perform on board? Thank you, Parvaneh Aghajani.

2 1

Blog on seL4 licensing
by Heiser, Gernot (Data61, Kensington NSW) 10 Dec '19

10 Dec '19

The question of what the seL4 license actually means, in particular, to which degree it may force deployer’s IP to be open-sourced (*), has come up repeatedly, and from informal discussions I realised that misconceptions abound. I tried to clear up such confusion in a blog that I just posted: https://microkerneldude.wordpress.com/2019/12/09/what-does-sel4s-license-im… Enjoy, Gernot (*) short answer: normally not at all!

1 0

try to add vm in zynqmp, but when run rootserve crash.
by yadong.li 03 Dec '19

03 Dec '19

hi： I try add vm in zynqmp, but when run rootserve crash. print See appendix for the log Function call stack create_objects for (int ut_index = 0; ut_index < spec->num_untyped; ut_index++) { .... CDL_Object *obj = &spec->objects[obj_id]; CDL_ObjectType capdl_obj_type = CDL_Obj_Type(obj); ----case crash } I fount when it access 0x440010 (the 42th of capdl_spec.objs, 0~41 objs access is OK) which is (CDL_Object)obj->type will case the crash, but I access the 42th obj->name ("frame_vm0_group_bin_0132" can be printed) is OK. [42] = { #ifdef CONFIG_DEBUG_BUILD .name = "frame_vm0_group_bin_0132", #endif .type = CDL_Frame, .size_bits = 21, .frame_extra = { .paddr = 0, }, }, what may be the problem ? mmu? Thank you very much. log: ## Starting application at 0x02793000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[2793000..481106f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 2878d08. Loaded DTB from 2878d08. paddr=[239000..23afff] ELF-loading image 'kernel' paddr=[0..238fff] vaddr=[ff8000000000..ff8000238fff] virt_entry=ff8000000000 ELF-loading image 'capdl-loader' paddr=[23b000..2393fff] vaddr=[400000..2558fff] virt_entry=408af8 ELF loader relocated, continuing boot... Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Warning: gpt_cntfrq 33333000, expected 100000000 Bootstrapping kernel Booting all finished, dropped to user space Caught cap fault in send phase at address (nil) while trying to handle: vm fault on data at address 0x440010 with status 0x93800007 in thread 0xff887f81b400 "rootserver" at address 0x4026e4 With stack: 0x2553d50: 0x424a9a 0x2553d58: 0x43ffb8 0x2553d60: 0x2553de0 0x2553d68: 0x408a4c 0x2553d70: 0x255a000 0x2553d78: 0x453588 0x2553d80: 0x0 0x2553d88: 0x25 0x2553d90: 0x900000000 0x2553d98: 0x100000000000009 0x2553da0: 0x800000000 0x2553da8: 0x43ffb8 0x2553db0: 0x2186 0x2553db8: 0x21dd 0x2553dc0: 0x2a 0x2553dc8: 0x408a40

1 0

Userspace debugging with QEMU/gdb
by Jiusheng Liu 02 Dec '19

02 Dec '19

Hi, >From the page https://docs.sel4.systems/DebuggingGuide.html (section Userspace debugging), I know we can debug userspace process by command below: ---------------------------- cmd example start ---------------------------------------- gdb ./dynamic-2 Reading symbols from ./dynamic-2...done. (gdb) target remote :1234 Remote debugging using :1234 0x000000000000fff0 in ?? () (gdb) break main Breakpoint 1 at 0x402011: file sel4-tutorials-manifest/dynamic-2/main.c, line 161. (gdb) c Continuing. Breakpoint 1, main () at sel4-tutorials-manifest/dynamic-2/main.c:161 161 (gdb) ---------------------------- cmd example end ---------------------------------------- It works for normal userspace process (such as the example code in tutorials: https://docs.sel4.systems/Tutorials/dynamic-2.html ). But when I want to debug the userspace process for the code in the tutorials page https://docs.sel4.systems/Tutorials/camkes-vm-linux.html (one virtual machine in seL4), I cannot catch the breakpoints. So can you help me to explain why I cannot catch the breakpoint? and can we debug the vmm create process with qemu/gdb? Thanks.

2 2

Re: [seL4] Devel Digest, Vol 66, Issue 26
by Millar, Curtis (Data61, Kensington NSW) 26 Nov '19

26 Nov '19

> As I'm playing with a prototype language and OS while building it on > top of seL4, > I'm not using any intermediate C layers to connect to the seL4 API (so > custom build and > integration and no C runtime), while most of the samples out there are > heavily relying on > some foundations, which is completely understandable, considering how > it can be involving > to build anything relevant on top of the seL4 API. > So as I'm just really getting started to integrate with seL4 (and > I love?? it!) I have to go through > all these details, but I hope that I won't be spamming unnecessarily > here! ? If you are looking to avoid any C interop or runtime that should be completely possible. The only requirement the kernel makes is that user- level code needs to keep track of the IPC buffer address on its own (unlike previous versions which ensure that a particular register contains the IPC buffer address). If you want a minimal runtime without TLS you could store the IPC buffer address in a global variable and ensure that your system call wrappers use that global variable to load and store data into the IPC buffer.

1 0

Re: [seL4] Understand how TLS is setup in the root server for x64
by Millar, Curtis (Data61, Kensington NSW) 25 Nov '19

25 Nov '19

Hi Alexandre, > I'm trying to understand how the TLS is setup for the root server on > x64 (to access for example the IPC buffer) > but I'm failing to connect the pieces and how the server is correctly > setting the FS register. There is detailed documentation for the TLS change on the page for RFC- 3. https://sel4.atlassian.net/browse/RFC-3 In essence, the new TLS model stores the address of the IPC buffer in a thread-local variable which must be initialised by your process or threading runtime along with general TLS intialisation. https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/functions.h#L… To assist with this there is a simple sel4runtime library which provides a minimal C-runtime and tools for initialising TLS. https://github.com/SEL4PROJ/sel4runtime On x86_64 the TLS register can be set without calling into the kernel by using the `wrfsbase` instruction or by using the `sel4runtime_set_tls_base` function from the sel4runtime library. > Now, I'm failing to find in the codebase where the ELF loader is > actually detecting the TLS segment and the according setup with the > TLS register. The ELF loader is not responsible for TLS initialisation, the C-runtime is responsible for configuring TLS of the initial thread. https://bitbucket.ts.data61.csiro.au/projects/SEL4PROJ/repos/sel4runtime/br… > Never mind, I discovered that I in order to access a TLS variable you > need to call `seL4_TCB_SetTLSBase` on seL4_CapInitThreadTCB first in > the root server, as I'm trying to work on a bare bone usage of seL4 to > better understand it, this part was not obvious from the existing more > complex samples! In general I would recommend having the initial thread in a process initialise its own TLS via the runtime and any new thread configure its own TLS in the initialisation code before the main function call of that thread with the `sel4runtime_set_tls_base`. Each new thread will also need to use `seL4_SetIPCBuffer` to initialise the IPC buffer address in its TLS before performing any invocations or any other system calls. Cheers, Curtis Millar Systems Engineer, Trustworthy Systems, CSIRO's Data61 curtis.millar(a)data61.csiro.au Data61, CSIRO Level 3, K17 Building UNSW Gate 14, Barker St Kensington NSW 2033 Australia

2 1

Is there a "modern" seL4 manifest/configuration that is known to run on CMA34CR?
by Nogin, Aleksey 24 Nov '19

24 Nov '19

Unless I am looking in the wrong place, all the CMA34CR support was removed in https://github.com/seL4/camkes-vm/commit/aab3478acc4705a3161f5bf59625f7c96a…. Is there something that remains? If not, what would be the best starting point to try to port a demo running on CMA34CR board from an old (early 2017) version of the sel4/camkes/etc to a recent stable release (e.g, 10.1.1)? Thanks. Aleksey CONFIDENTIALITY NOTICE: The information transmitted in this email, including attachments, is intended only for the person(s) or entity to which it is addressed and may contain confidential, proprietary and/or privileged material exempt from disclosure under applicable law. Any review, retransmission, dissemination or other use of, or taking of any action in reliance upon this information by persons or entities other than the intended recipient is prohibited. If you received this message in error, please contact the sender immediately and destroy any copies of this information in their entirety.

2 4

Understand how TLS is setup in the root server for x64
by Alexandre Mutel 23 Nov '19

23 Nov '19

Hello! I'm trying to understand how the TLS is setup for the root server on x64 (to access for example the IPC buffer) but I'm failing to connect the pieces and how the server is correctly setting the FS register. For example the sel4_Send function is codegen like this (using -ftls-model=local-exec) Function: seL4_Send push r15 mov rdx,0FFFFFFFFFFFFFFFDh push rbx mov rax,[fs:0] mov r10,[rax+8] mov r8,[rax+10h] mov r9,[rax+18h] mov r15,[rax+20h] mov rbx,rsp syscall mov rsp,rbx pop rbx pop r15 ret The instruction `mov rax,[fs:0]` is accessing the seL4_IPCBuffer* and the the executable has a TLS segments of 8 bytes for the pointer. all good. Now, I'm failing to find in the codebase where the ELF loader is actually detecting the TLS segment and the according setup with the TLS register. And I'm wondering if the setup for the codegen is not wrong on my side (e.g the local-exec is not working), so that instead of having a FS register it would be a direct memory access. Does anyone have a clue about this? Thank you!

1 2

Fwd: port sel4 to RK3308(quad cortex-a35)
by Yun Zhou 22 Nov '19

22 Nov '19

---------- Forwarded message --------- 发件人： Yun Zhou <shiny725829(a)gmail.com> Date: 2019年10月25日周五下午9:52 Subject: port sel4 to RK3308(quad cortex-a35) To: <devel-owner(a)sel4.systems> Dear sel4 Experts How are you I found some information about sel4, and sel4 is great microkernel OS, i want port sel4 to RK3308(quad cortex-a35, GICv2) for real time audio signal processing. Form the Tutorials I found sel4 just support cortex-a53, I would like to ask does sel4 support cortex-a35 SMP mode. and because our application is real time audio processing so system delay must lower than 3ms and hard real-time determinism. Will sel4 support real-time signal processing? Looking forward to your reply Thanks &Kind regards Yun

2 1

Nasty bug in global-components/templates/rpc-signalling.template.c
by Nogin, Aleksey 22 Nov '19

22 Nov '19

After spending a few hours debugging time server not working for me, I realized that global-components/templates/rpc-signalling.template.c that was added earlier this year contains the following /*- set badge = str(configuration[c.instance.name].get("%s_attributes" % c.interface.name)).strip('"') -*/ [...] /*- do badges.sort() -*/ [...] int /*? me.interface.name ?*/_largest_badge(void) { return /*? badges[len(badges) - 1] ?*/; } Unfortunately for me, my Trusted Build generated camkes had the attributes numbered 1,2,3,10,11,12,13 and therefore the above core was claiming that the time_server_largest_badge is 3 :(. Obviously, the issue is the combination of the str and sort, resulting in the last badge being the one largest lexicographically, not numerically :(. Replacing the str with int (and correspondingly removing the strip) solved the problem for me. P.S. Well, solved that particular problem for me, not the problem of time server not working - looks like now I will have to debug FAULT HANDLER: data fault from time_server.time_server_0_control (ID 0x2) on address 0x84b8ba, pc = 0x42439d, fsr = 0x4 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x42439d FAULT HANDLER: rsp :0x454cf0 FAULT HANDLER: rflags :0x10202 FAULT HANDLER: rax :0x413a33 FAULT HANDLER: rbx :0x437e88 FAULT HANDLER: rcx :0x0 FAULT HANDLER: rdx :0x437e98 FAULT HANDLER: rsi :0x28 FAULT HANDLER: rdi :0x437e98 FAULT HANDLER: rbp :0x454d70 FAULT HANDLER: r8 :0xffffffff FAULT HANDLER: r9 :0x0 FAULT HANDLER: r10 :0xe8 FAULT HANDLER: r11 :0x293 FAULT HANDLER: r12 :0x413a32 FAULT HANDLER: r13 :0x84b8ba FAULT HANDLER: r14 :0x0 FAULT HANDLER: r15 :0x0 FAULT HANDLER: fs_base :0x44a460 FAULT HANDLER: gs_base :0x0 FAULT HANDLER: memory map: FAULT HANDLER: +-- 0x0000000000458fff -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000458000 -- FAULT HANDLER: | IPC buffer FAULT HANDLER: +-- 0x0000000000457000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000456000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000455000 -- FAULT HANDLER: | stack FAULT HANDLER: +-- 0x0000000000451000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000450000 -- FAULT HANDLER: | code and data FAULT HANDLER: +-- 0x0000000000400000 - :( Aleksey CONFIDENTIALITY NOTICE: The information transmitted in this email, including attachments, is intended only for the person(s) or entity to which it is addressed and may contain confidential, proprietary and/or privileged material exempt from disclosure under applicable law. Any review, retransmission, dissemination or other use of, or taking of any action in reliance upon this information by persons or entities other than the intended recipient is prohibited. If you received this message in error, please contact the sender immediately and destroy any copies of this information in their entirety.

2 1

(no subject)
by abdi mahmud haji 22 Nov '19

22 Nov '19

I was trying to build camkes-vm-crossvm tutorials by using "./init --tut camkes-vm-crossvm" and it initiate some folder with some file and some folder is empty and some are missing.So can someone help me how to fix it,and this the following is it output. ============================================== ./init --tut camkes-vm-crossvm loading initial cache file ../settings.cmake -- The C compiler identification is GNU 5.4.0 -- Check for working C compiler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- The CXX compiler identification is GNU 5.4.0 -- Check for working CXX compiler: /usr/bin/g++ -- Check for working CXX compiler: /usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- Found musllibc: /home/sel4/sel4-tutorials-manifest/projects/musllibc -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- CPIO test cpio_reproducible_flag FAILED -- /home/sel4/sel4-tutorials-manifest/camkes-vm-crossvm_build/camkes-vm-crossvm/ast.pickle is out of date. Regenerating... ERROR:CAmkES:/home/sel4/sel4-tutorials-manifest/camkes-vm-crossvm/crossvm_tutorial.camkes:27:1: } ERROR:CAmkES: ^ ERROR:CAmkES:Syntax error in input at '}' (type _ANON_1) line 34 col 1 CMake Error at tools/camkes/camkes.cmake:494 (message): Failed to generate /home/sel4/sel4-tutorials-manifest/camkes-vm-crossvm_build/camkes-vm-crossvm/ast.pickle Call Stack (most recent call first): camkes-vm-crossvm/CMakeLists.txt:37 (GenerateCAmkESRootserver) -- Configuring incomplete, errors occurred! See also "/home/sel4/sel4-tutorials-manifest/camkes-vm-crossvm_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/home/sel4/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/home/sel4/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 75, in _init_build_directory return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output) File "/home/sel4/.local/lib/python3.5/site-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/home/sel4/.local/lib/python3.5/site-packages/sh.py", line 774, in __init__ self.wait() File "/home/sel4/.local/lib/python3.5/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/home/sel4/.local/lib/python3.5/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DFORCE_IOMMU=ON -DTUTORIAL_DIR=camkes-vm-crossvm -C ../settings.cmake .. STDOUT: STDERR: =============================================

2 1

compile camkes_arm_vm project(tx1 vm_minimal), The file format is not correct
by yadong.li 22 Nov '19

22 Nov '19

Hi I compile camkes_arm_vm with tx1 vm_minimal Command: ../init-build.sh -DAARCH64=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tx1 Buf output file is not elf # aarch64-linux-gnu-objcopy -O binary images/capdl-loader-image-arm-tx1 sel4-vmm-minimal aarch64-linux-gnu-objcopy:images/capdl-loader-image-arm-tx1: File format not recognized see appendix for the log Thank you very much Log: 1、配置环境 #<mailto:root@HP-Z240:/home/yadong.li/seL4/camkes_arm_vm/build_temp> ../init-build.sh -DAARCH64=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tx1 loading initial cache file /home/yadong.li/seL4/camkes_arm_vm/projects/vm/settings.cmake correct_platform_strings: Based on toolchain, setting KernelSel4Arch: aarch64 -- Found seL4: /home/yadong.li/seL4/camkes_arm_vm/kernel …………. -- Found camkes-arm-vm: /home/yadong.li/seL4/camkes_arm_vm/projects/vm -- Found camkes-tool: /home/yadong.li/seL4/camkes_arm_vm/projects/camkes-tool -- Found global-components: /home/yadong.li/seL4/camkes_arm_vm/projects/global-components -- Found camkes-vm: /home/yadong.li/seL4/camkes_arm_vm/projects/camkes-vm -- Found camkes-vm-images: /home/yadong.li/seL4/camkes_arm_vm/projects/camkes-vm-images -- Found sel4_projects_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/seL4_projects_libs -- Found elfloader-tool: /home/yadong.li/seL4/camkes_arm_vm/tools/seL4/elfloader-tool -- Found musllibc: /home/yadong.li/seL4/camkes_arm_vm/projects/musllibc -- Found util_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/util_libs -- Found seL4_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/seL4_libs -- Found projects_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/projects_libs -- Found capdl: /home/yadong.li/seL4/camkes_arm_vm/projects/capdl -- /home/yadong.li/seL4/camkes_arm_vm/build_temp/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... -- CPIO test cpio_reproducible_flag PASSED -- Found sel4runtime: /home/yadong.li/seL4/camkes_arm_vm/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- /home/yadong.li/seL4/camkes_arm_vm/build_temp/ast.pickle is out of date. Regenerating... -- /home/yadong.li/seL4/camkes_arm_vm/build_temp/camkes-gen.cmake is out of date. Regenerating... -- Configuring done -- Generating done -- Build files have been written to: /home/yadong.li/seL4/camkes_arm_vm/build_temp 2、编译 #<mailto:root@HP-Z240:/home/yadong.li/seL4/camkes_arm_vm/build_temp> ninja [41/320] Performing CAmkES generation for 15 files [58/320] Generating capDL-tool/parse-capDL stack build --fast Building all executables for `capDL-tool' once. After a successful build of all of them, only specified executables will be rebuilt. capDL-tool-1.0.0.1: configure (exe) Configuring capDL-tool-1.0.0.1... capDL-tool-1.0.0.1: build (exe) Preprocessing executable 'parse-capDL' for capDL-tool-1.0.0.1... [ 1 of 16] Compiling CapDL.Model ( CapDL/Model.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Model.o ) [ 2 of 16] Compiling CapDL.State ( CapDL/State.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/State.o ) [ 3 of 16] Compiling CapDL.PrintUtils ( CapDL/PrintUtils.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintUtils.o ) [ 4 of 16] Compiling CapDL.PrintC ( CapDL/PrintC.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintC.o ) [ 5 of 16] Compiling CapDL.PrintDot ( CapDL/PrintDot.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintDot.o ) [ 6 of 16] Compiling CapDL.PrintIsabelle ( CapDL/PrintIsabelle.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintIsabelle.o ) [ 7 of 16] Compiling CapDL.PrintModel ( CapDL/PrintModel.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintModel.o ) [ 8 of 16] Compiling CapDL.PrintXml ( CapDL/PrintXml.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintXml.o ) [ 9 of 16] Compiling CapDL.Matrix ( CapDL/Matrix.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Matrix.o ) [10 of 16] Compiling CapDL.STCC ( CapDL/STCC.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/STCC.o ) [11 of 16] Compiling CapDL.AST ( CapDL/AST.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/AST.o ) [12 of 16] Compiling CapDL.MakeModel ( CapDL/MakeModel.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/MakeModel.o ) [13 of 16] Compiling CapDL.ParserUtils ( CapDL/ParserUtils.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/ParserUtils.o ) [14 of 16] Compiling CapDL.DumpParser ( CapDL/DumpParser.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/DumpParser.o ) [15 of 16] Compiling CapDL.Parser ( CapDL/Parser.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Parser.o ) [16 of 16] Compiling Main ( Main.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/Main.o ) Linking .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL ... capDL-tool-1.0.0.1: copy/register Installing executable(s) in /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin stack install Copying from /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin/parse-capDL to /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool/parse-capDL Copied executables to /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool: - parse-capDL Warning: Installation path /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool not found on the PATH environment variable. [68/320] Building C object CMakeFiles/vm0.instance.bin.dir/components/VM/src/main.c.obj ………………….. musllibc/build-temp/stage/include/inttypes.h:133:27: note: format string is defined here #define PRIuPTR __PRIPTR "u" [320/320] Generating images/capdl-loader-image-arm-tx1 #file images/capdl-loader-image-arm-tx1 images/capdl-loader-image-arm-tx1: data #arch64-linux-gnu-objcopy -O binary images/capdl-loader-image-arm-tx1 sel4-vmm-minimal aarch64-linux-gnu-objcopy:images/capdl-loader-image-arm-tx1: File format not recognized

2 1

Camkes and GPIO
by Parvaneh Ahgajani 21 Nov '19

21 Nov '19

Hello all, I am trying to implement a simple demo on sel4 using camkes. I need to add some external hardware like sensors to my demo. For this purpose I need GPIO programming. Could you please point me to some example GPIO components? Should I add hardware component? or just use <platsupport.GPIO.h> to write signal on pins on source files? Thank you for your time and consideration, Parveneh.

2 5

releasing confidentiality
by Michael Neises 15 Nov '19

15 Nov '19

Hi, I know that seL4 provides confidentiality, which is described as a property that "means that data cannot be read without permission." Given this wording, I wonder if it is not possible to revoke those permissions in certain cases. In particular, I would like for one camkes component to be able to perform runtime measurements, such as heap analysis, on another component. Or even better, I would like for a component to be able to perform runtime measurements on a program running within the camkes linux vm. Is such a feat possible? Best, Michael Neises

3 2

Fwd: camkes vm question
by Michael Neises 15 Nov '19

15 Nov '19

Hello, In my system, sel4 is loaded by u-boot from an sd card that contains only an ELF image. I would like to store some sensitive data in plaintext for use in a non-vm component, but I worry that it can be read from the ELF image. Can this sd card data be accessed from within a linux vm instance? Or otherwise, is it certain that the vm cannot access this data? Best, Michael Neises

2 2

TLB issue
by Stefan Kalkowski 15 Nov '19

15 Nov '19

Dear sel4 community, yesterday I've started to develop a low-level platform test to stress several multi-processor aspects on top of the Genode API. Thereby, I've recognized that on sel4/x86_64 the TLB is practically not always cleaned properly in SMP systems. The test spawns threads of one protection domain on each available cpu. Each thread accesses one of the first words of a shared dataspace. Afterwards the main thread on CPU 0 detaches and destroys the dataspace. Unfortunately, the threads on other CPUs still successfully access the corresponding memory instead of triggering a fault. To be able to reproduce the problem, you might investigate the simple test case here: https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7… My colleague Alexander Boettcher already investigated the problem in part, and might share his insights with you. Best regards Stefan -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

3 3

Re: [seL4] RISC-V port
by Zhuang, Siwei (Data61, Kensington NSW) 14 Nov '19

14 Nov '19

It looks like either you're using the libarchive in python2 or the package is outdated. Try something like, pip3 install libarchive --upgrade You may need to remove the libarchive from python2, although seL4test requires both python2 and 3. Regards, Siwei On Wed, 2019-11-13 at 20:26 -0800, Jacob Yu wrote: > Thanks, Siwei. > > After I have done a clean build (by removing previous installation in > "/opt/riscv"), I am able to enable "multilib" when building > "riscv-gnu-toolchain" successfully. I also found out that I needed to > build Newlib. > > I can now run " ../init-build.sh -DPLATFORM=spike -DRISCV64=TRUE > -DSIMULATION=1" in the build directory under seL4Test but still failed in > ninja: > > [1/20] Generating gen_headers/image_start_addr.h > FAILED: elfloader/gen_headers/image_start_addr.h > cd /home/webuser/Dev/l4/l4dev/seL4test/cbuild/elfloader && sh -c > "/home/webuser/Dev/l4/l4dev/seL4test/tools/seL4/elfloader-tool/../cmake- > tool/helpers/shoehorn.py > /home/webuser/Dev/l4/l4dev/seL4test/cbuild/kernel/gen_headers/plat/machine/p > latform_gen.yaml > /home/webuser/Dev/l4/l4dev/seL4test/cbuild/elfloader/archive.o > > /home/webuser/Dev/l4/l4dev/seL4test/cbuild/elfloader/gen_headers//image_star > t_addr.h" > Traceback (most recent call last): > File > "/home/webuser/Dev/l4/l4dev/seL4test/tools/seL4/elfloader-tool/../cmake- > tool/helpers/shoehorn.py", > line 81, in <module> > def get_bytes(entry: libarchive.entry.ArchiveEntry) -> io.BytesIO: > AttributeError: module 'libarchive' has no attribute 'entry' > ninja: build stopped: subcommand failed. > > Thank again for all the help. > > Regards, > > > Jacob > > On Tue, Nov 12, 2019 at 4:37 PM Zhuang, Siwei (Data61, Kensington NSW) < > Siwei.Zhuang(a)data61.csiro.au> wrote: > > > Hi Jacob, > > > > Never had this problem before, so just a blind guess. > > > > As you can build "riscv-pk", you must be using the cross compiler from > > your > > previous build(with multilib disabled). Try removing the previous > > installation in "/opt/riscv", and also do "make clean" to remove all the > > previous build directories. > > > > I noticed that the log you attached says "Checking whether the C compiler > > works ... no", have a look at "config.log" to see if there's any useful > > info. > > > > Also make sure you have enough disk space, my build takes 21GB. > > > > Regards, > > Siwei > > > > On Tue, 2019-11-12 at 11:31 -0800, Jacob Yu wrote: > > > Hi > > > > > > I am able to install & build "riscv-pk" and "riscv-isa-sim", and then > > > try > > > out Spike. Many thank! > > > > > > > ./configure --prefix=/opt/riscv --enable-multilib > > > > sudo make linux > > > Otherwise, I also tried to enable "multilib" when building > > > "riscv-gnu-toolchain" but with no luck. It complained: > > > > > > > ... > > > > configure: error: in > > > `/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux- > > > stage2/riscv64-unknown-linux-gnu/lib32/ilp32/libgomp': > > > > configure: error: C compiler cannot create executables > > > > > > And make failed with: > > > > > > > Makefile:13703: recipe for target 'configure-target-libgomp' failed > > > > make[2]: *** [configure-target-libgomp] Error 1 > > > > > > Again, any suggestions? > > > > > > Regards, > > > > > > > > > Jacob > > > ============================================================ > > > ... > > > checking for riscv64-unknown-linux-gnu-gcc... > > > /home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux- > > > stage2/./gcc/xgcc > > > > > -B/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux- > > stage2/./gcc/ > > > -B/opt/riscv/riscv64-unknown-linux-gnu/bin/ > > > -B/opt/riscv/riscv64-unknown-linux-gnu/lib/ -isystem > > > /opt/riscv/riscv64-unknown-linux-gnu/include -isystem > > > /opt/riscv/riscv64-unknown-linux-gnu/sys-include -march=rv32imac > > > -mabi=ilp32 > > > > > > > > > > > > *checking whether the C compiler works... noconfigure: error: in > > > `/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux- > > > stage2/riscv64-unknown-linux-gnu/lib32/ilp32/libgomp':configure: > > > error: C compiler cannot create executablesSee `config.log' for more > > > details* > > > > > > *Makefile:13703: recipe for target 'configure-target-libgomp' > > > failedmake[2]: *** [configure-target-libgomp] Error 1* > > > make[2]: Leaving directory > > > '/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux-stage2' > > > Makefile:951: recipe for target 'all' failed > > > make[1]: *** [all] Error 2 > > > make[1]: Leaving directory > > > '/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux-stage2' > > > Makefile:304: recipe for target 'stamps/build-gcc-linux-stage2' failed > > > make: *** [stamps/build-gcc-linux-stage2] Error 2 > > > > > > On Mon, Nov 11, 2019 at 5:52 PM Zhuang, Siwei (Data61, Kensington NSW) < > > > Siwei.Zhuang(a)data61.csiro.au> wrote: > > > > > > > No, building riscv-isa-sim alone is sufficient if you only need Spike. > > > > > > > > seL4 also generates a script called "simulate" in the your build > > > > directory. > > > > The script invokes qemu for simulation. > > > > > > > > Regards, > > > > Siwei > > > > > > > > On Mon, 2019-11-11 at 17:20 -0800, Jacob Yu wrote: > > > > > Thanks, Siwei for the info. I'll give it a try. > > > > > > > > > > > Running seL4 no longer requires RISC-V tools. In case you want to > > use > > > > > Spike, > > > > > > I'd suggest building the riscv-isa-sim separately to get the > > > > > > latest > > > > code. > > > > > Does this require RISC-V tools to build? > > > > > > > > > > Best, > > > > > > > > > > > > > > > Jacob > > > > > > > > > > On Sun, Nov 10, 2019 at 10:58 PM Zhuang, Siwei (Data61, Kensington > > NSW) > > > > > < > > > > > Siwei.Zhuang(a)data61.csiro.au> wrote: > > > > > > > > > > > Hi Jacob, > > > > > > > > > > > > You need to enable multilib when building "riscv-gnu-toolchain". > > > > > > > > > > > > ./configure --prefix=/path-to-install-toolchain > > --enable-multilib > > > > > > then > > > > > > make or make linux > > > > > > > > > > > > Running seL4 no longer requires RISC-V tools. In case you want to > > use > > > > > > Spike, > > > > > > I'd suggest building the riscv-isa-sim separately to get the > > > > > > latest > > > > code. > > > > > > Regards, > > > > > > Siwei > > > > > > > > > > > > On Sun, 2019-11-10 at 15:50 -0800, Jacob Yu wrote: > > > > > > > Hi > > > > > > > > > > > > > > I am trying to build "seL4 tests" for "Spike" platform (the > > RISC-V > > > > > > > simulator from UC Berkeley) on Ubuntu 18.04.3 LTS, a 64-bit > > system. > > > > > > > First of all, I was able to build RISC-V tools with "build.sh" > > after > > > > > > > manually installing "riscv-gnu-toolchain" from GitHub as well as > > > > > > additional > > > > > > > python modules (future, ply, protobuf). I then kicked of > > > > > > "../init-build.sh > > > > > > > -DPLATFORM=spike -DRISCV64=TRUE -DSIMULATION=1" from local build > > > > > > directory. > > > > > > > After that, however, "ninja" command complained about "undefined > > > > > > reference > > > > > > > to `__nedf2'". I understand there is no FPU support in "Spike" > > > > platform > > > > > > so > > > > > > > a need for "soft-float" module. Where should I specify > > "-lsoft-fp"? > > > > > > > Any suggestions? > > > > > > > > > > > > > > Thanks, > > > > > > > > > > > > > > > > > > > > > Jacob > > > > > > > _______________________________________________ > > > > > > > Devel mailing list > > > > > > > Devel(a)sel4.systems > > > > > > > https://sel4.systems/lists/listinfo/devel

2 1

RISC-V port
by Jacob Yu 13 Nov '19

13 Nov '19

Hi I am trying to build "seL4 tests" for "Spike" platform (the RISC-V simulator from UC Berkeley) on Ubuntu 18.04.3 LTS, a 64-bit system. First of all, I was able to build RISC-V tools with "build.sh" after manually installing "riscv-gnu-toolchain" from GitHub as well as additional python modules (future, ply, protobuf). I then kicked of "../init-build.sh -DPLATFORM=spike -DRISCV64=TRUE -DSIMULATION=1" from local build directory. After that, however, "ninja" command complained about "undefined reference to `__nedf2'". I understand there is no FPU support in "Spike" platform so a need for "soft-float" module. Where should I specify "-lsoft-fp"? Any suggestions? Thanks, Jacob

2 5

Re: [seL4] RISC-V port
by Jesse Millwood 11 Nov '19

11 Nov '19

I do believe you can use SiFive's toolchain: https://static.dev.sifive.com/dev-tools/riscv64-unknown-elf-gcc-8.3.0-2019.… Then you don't have to compile it. There is also Data61's Docker https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles If you look at the make file there are some targets for including the RISC-V toolchain. Jesse On 2019-11-11 1:58 a.m., Zhuang, Siwei (Data61, Kensington NSW) wrote: > Hi Jacob, > > You need to enable multilib when building "riscv-gnu-toolchain". > > ./configure --prefix=/path-to-install-toolchain --enable-multilib > then > make or make linux > > Running seL4 no longer requires RISC-V tools. In case you want to use Spike, > I'd suggest building the riscv-isa-sim separately to get the latest code. > > Regards, > Siwei > > On Sun, 2019-11-10 at 15:50 -0800, Jacob Yu wrote: >> Hi >> >> I am trying to build "seL4 tests" for "Spike" platform (the RISC-V >> simulator from UC Berkeley) on Ubuntu 18.04.3 LTS, a 64-bit system. >> >> First of all, I was able to build RISC-V tools with "build.sh" after >> manually installing "riscv-gnu-toolchain" from GitHub as well as additional >> python modules (future, ply, protobuf). I then kicked of "../init-build.sh >> -DPLATFORM=spike -DRISCV64=TRUE -DSIMULATION=1" from local build directory. >> >> After that, however, "ninja" command complained about "undefined reference >> to `__nedf2'". I understand there is no FPU support in "Spike" platform so >> a need for "soft-float" module. Where should I specify "-lsoft-fp"? >> >> Any suggestions? >> >> Thanks, >> >> >> Jacob >> _______________________________________________ >> Devel mailing list >> Devel(a)sel4.systems >> https://sel4.systems/lists/listinfo/devel > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel

1 0

Rust ports on Genode/seL4
by guo minskey 11 Nov '19

11 Nov '19

Hi, guys, I am trying to build genode/sel4 on x86_64 platform and expect to get a GUI working. And so I enable this option in my build.conf : REPOSITORIES += $(GENODE_DIR)/repos/libports. Seems that rust support is broken (because rustc version ??). Which version of rustc should I use to build rust ports on genode ? Or how can I disable rust ports in build.conf configuration or somewhere else ? thanks, -Minskey

3 3

a letter for seeking help about sel4
by 李庚 08 Nov '19

08 Nov '19

Dear Sir or Madam, Very Sorry to brother you. We have get into trouble after compiling sel4 following the https://docs.sel4.systems/Docker.html,may I seek some advice from you? First,I attmpt to follow the https://docs.sel4.systems/Hardware/VMware/,however,error "Failed to allocate object of size xxxx" ara discovered in serial_output.txt . Second,we wanna to make a sel4 startup disk for x86_64,is there any useful Document ? Sorry again for this sudden interruption and I would be very grateful if receive your reply. Yours Sinerely, Andrew

2 1

Building seL4test x86_64 on Debian with the Docker image
by Jacob Yu 05 Nov '19

05 Nov '19

Hi I am building "seL4test" using the Docker image on Ubuntu 18.04.3 LTS, a 64-bit system. After entering "../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE" in a build directory within Docker it complained "Could NOT find NANOPB (missing: PROTOBUF_PROTOC_EXECUTABLE)". I wonder should I manually download and install protocol buffer compiler, protoc? Please advise. Thank for your help. Jacob =============================================== loading initial cache file /host/projects/sel4test/settings.cmake correct_platform_strings: Attempting to correct PLATFORM: x86_64 to new valid KernelPlatform: pc99 KernelSel4Arch: x86_64 -- Found seL4: /host/kernel -- The C compiler identification is GNU 6.5.0 -- The CXX compiler identification is GNU 6.5.0 -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /usr/bin/g++ -- Check for working CXX compiler: /usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- Found elfloader-tool: /host/tools/seL4/elfloader-tool -- Found musllibc: /host/projects/musllibc -- Found util_libs: /host/projects/util_libs -- Found seL4_libs: /host/projects/seL4_libs -- Found sel4_projects_libs: /host/projects/sel4_projects_libs -- Found sel4runtime: /host/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- Found PythonInterp: /usr/bin/python (found version "2.7.15") -- Could NOT find NANOPB (missing: PROTOBUF_PROTOC_EXECUTABLE) -- CPIO test cpio_reproducible_flag PASSED -- Configuring done -- Generating done -- Build files have been written to: /host/build-x86

2 2

Re: [seL4] Devel Digest, Vol 65, Issue 24
by Mcleod, Kent (Data61, Kensington NSW) 04 Nov '19

04 Nov '19

> abdi@abdi-HP-P-PC:~/sel4-tutorials-manifest$ ./init --tut hello-world > loading initial cache file ../settings.cmake > CMake Error: Error: generator : Ninja > Does not match the generator used previously: Unix Makefiles > Either remove the CMakeCache.txt file and CMakeFiles directory or choose a different binary directory. These errors indicate that CMake already believes a project has been created in the target directory and that this project was a Makefile based project. Is there any CMakeCache.txt files located anywhere in the project structure that may be causing CMake to get confused? Otherwise you could reinitialise the tutorial project and try initialising hello-world again and that would also fix your problem.

1 0

Re: [seL4] Devel Digest, Vol 65, Issue 24
by abdi mahmud haji 31 Oct '19

31 Oct '19

i am working on sel4-tutorials for the first time .i setup my machine accordingly and then when i trying to generate the tutorials like this "./init --tut hello-world" i keep getting an error message and dont know what to do or how to fix it . the error was like bellowing =================================================== abdi@abdi-HP-P-PC:~/sel4-tutorials-manifest$ ./init --tut hello-world loading initial cache file ../settings.cmake CMake Error: Error: generator : Ninja Does not match the generator used previously: Unix Makefiles Either remove the CMakeCache.txt file and CMakeFiles directory or choose a different binary directory. Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/home/abdi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/home/abdi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 75, in _init_build_directory return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 774, in __init__ self.wait() File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /home/abdi/.local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-world82varrcf -C ../settings.cmake .. STDOUT: STDERR: ====================================================================== is there someone who suggests what i should do please. thanks On Sun, Oct 27, 2019 at 4:00 AM <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: releasing confidentiality > (Heiser, Gernot (Data61, Kensington NSW)) > 2. Fwd: port sel4 to RK3308(quad cortex-a35) (Yun Zhou) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sat, 26 Oct 2019 03:07:23 +0000 > From: "Heiser, Gernot (Data61, Kensington NSW)" > <Gernot.Heiser(a)data61.csiro.au> > To: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] releasing confidentiality > Message-ID: <5FEA58C5-9011-49B7-9790-28B4B54849EF(a)data61.csiro.au> > Content-Type: text/plain; charset="utf-8" > > On 26 Oct 2019, at 08:00, Michael Neises <neisesmichael(a)gmail.com> wrote: > > > > Hi, > > > > I know that seL4 provides confidentiality, which is described as a > property that "means that data cannot be read without permission." Given > this wording, I wonder if it is not possible to revoke those permissions in > certain cases. In particular, I would like for one camkes component to be > able to perform runtime measurements, such as heap analysis, on another > component. Or even better, I would like for a component to be able to > perform runtime measurements on a program running within the camkes linux > vm. Is such a feat possible? > > Hi Michael > > seL4’s confidentiality (and other security) enforcement means that the > kernel guarantees that you can only access objects to which you have been > given explicit permission (in the form of a capability). How those > permissions are allocated is a matter of policy, the kernel doesn’t care, > it only enforces. > > In particular, it is totally possible in seL4 to give one component access > to another component’s address space, that’s for the user-level policy > framework to decide. > > Whether the present CAmkES framework supports this is a different > question, which I’ll leave to someone who’s more up to date with CAmkES > details. > > Gernot > > > ------------------------------ > > Message: 2 > Date: Sat, 26 Oct 2019 10:35:50 +0800 > From: Yun Zhou <shiny725829(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Fwd: port sel4 to RK3308(quad cortex-a35) > Message-ID: > <CAHNKqcxb7ws3MD=- > nwJka6HKEcA4hXZipJv0vdsStetJjxP-yg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > ---------- Forwarded message --------- > 发件人： Yun Zhou <shiny725829(a)gmail.com> > Date: 2019年10月25日周五下午9:52 > Subject: port sel4 to RK3308(quad cortex-a35) > To: <devel-owner(a)sel4.systems> > > > Dear sel4 Experts > How are you > I found some information about sel4, and sel4 is great microkernel OS, i > want port sel4 to RK3308(quad cortex-a35, GICv2) for real time audio signal > processing. Form the Tutorials I found sel4 just support cortex-a53, I > would like to ask does sel4 support cortex-a35 SMP mode. and because our > application is real time audio processing so system delay must lower than > 3ms and hard real-time determinism. > Will sel4 support real-time signal processing? > Looking forward to your reply > > Thanks &Kind regards > Yun >

1 0

The seL4 Foundation is coming!
by Heiser, Gernot (Data61, Kensington NSW) 25 Oct '19

25 Oct '19

Re-post from announce(a)sel4.systems<mailto:announce@sel4.systems> regarding the seL4 Foundation. We’ll start recruiting members soon. Gernot Begin forwarded message: From: Announcements about seL4 -- low volume list <announce(a)sel4.systems<mailto:announce@sel4.systems>> Subject: [seL4 Announce] The seL4 Foundation is coming! Date: 25 October 2019 at 17:09:30 AEDT To: "announce(a)sel4.systems<mailto:announce@sel4.systems>" <announce(a)sel4.systems<mailto:announce@sel4.systems>> Reply-To: <announce(a)sel4.systems<mailto:announce@sel4.systems>> Dear seL4 community, With great excitement we announce that we are in the process of setting up an seL4 Foundation, similar to foundations for other open-source projects, such as Linux and RISC-V. This will form an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It will bring together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those deploying seL4-based systems. Its focus will be on coordinating, directing and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raising funds for accelerating development, and ensuring clarity of verification claims. This was originally announced at the seL4 Summit in the US last month. I apologise for the delay in this posting (side-tracked with various issues). Gernot on behalf of the Trustworthy Systems team _______________________________________________ Announce mailing list Announce(a)sel4.systems<mailto:Announce@sel4.systems> https://sel4.systems/lists/listinfo/announce

1 0

Upcoming release planned
by Mcleod, Kent (Data61, Kensington NSW) 23 Oct '19

23 Oct '19

Hi all, I'm announcing that we are planning a new versioned release of seL4, capDL and CAmkES in about 3 weeks - around 11 November. We want to provide an opportunity for people to report issues or provide patches that can be fixed/incorporated for the versioned release. The last versioned release occurred almost 12 months ago and we plan on returning to a shorter release cycle of several weeks per cycle. Feel free to raise new issues across our GitHub repositories and we will also try to address any currently outstanding issues that have been neglected. Here is a highlight list of what changes are going to be in the upcoming versioned release: ## seL4 - Add GrantReply access right for endpoint capabilities. `seL4_Call` is permitted on endpoints with either the Grant or the GrantReply access rights. Capabilities can only be transferred in a reply message if receiver's endpoint capability has the Grant right. The GrantReply access right allows endpoints to be configured for two-way communication without also providing the right to transfer authority via capability transfer. - Merging of the mixed-criticality scheduling (MCS) branch into master. Previously the MCS branch only received versioned releases. Merging it into master under a build configuration (KernelIsMCS) makes it easier to keep up to date with changes to master and other tooling/libraries in-between versioned releases. Verification work is still on-going. - Continued development of the newly added RISC-V platform to support in-progress verification. - Auto-generation of Arm and RISC-V kernel platform definitions from a provided devicetree as well as support for passing a devicetree to the root task via the seL4_BootInfo structure. Interrupt controllers, timers and other devices required by the kernel can also be selected in the devicetree provided that the kernel already has a compatible driver. - Support for AArch64 hypervisors is in active development with initial support for Cortex-A53 and Cortex-A57 cores - De-duplicating kernel platform configurations and code in order to reduce the effort required to support additional platforms. - New platforms added: BeagleBone Blue, Hardkernel ODROID-C2, Freescale i.MX8M, i.MX8M Mini, Arm FVP (based on foundation-v8-gicv3.dts), QEMU ARM virt platform (with 3 CPUs: cortex-A15, cortex-A53 and cortex-A57) and possibly PINE64 ROCKPro64. - Implement RFC-3: Cross-platform thread-local storage (TLS) support. https://sel4.atlassian.net/browse/RFC-3. This provides a way for a thread to access or modify a thread-specific pointer without requiring a capability to itself. On architectures that don't provide unprivileged write access to this pointer a new syscall `seL4_SetTLSBase` is added that performs this operation. The kernel no longer reserves a register for holding a thread's IPC buffer and it is the thread's responsibility for managing this. `libsel4` declares a pointer to a thread's IPC buffer using a `__thread` keyword and a new user-level library `sel4runtime` can be used to provide a minimal supporting runtime. Additionally, the IPC buffer's userData field is no longer used for holding a pointer to the IPC buffer. - Better SMP Arm IRQ handling: Support is added for creating IRQ handler capabilities for core-local interrupts (PPIs) for each core and for also specifying a target core for global interrupts (SPIs) via the new invocation `IRQControl_GetTriggerCore`. - Merge ARCH_Page_Remap functionality into ARCH_Page_Map. Remap was used for updating the mapping attributes of a page without changing its virtual address. Now ARCH_Page_Map can be performed on an existing mapping to achieve the same result. The ARCH_Page_Remap invocation has been removed from all configurations. - Support for compiling the kernel with Clang. For a more complete list see the CHANGES file in the seL4 repository. ## CAmkES - Support for the new seL4 Endpoint GrantReply access right for CAmkES connector types. This allows multi-sender/single-receiver connectors such as `seL4RPCCall` that don't also provide the ability for arbitrary capability transfer from sender to receiver. Previously the `seL4RPC` connector was used instead of `seL4RPCCall` to create an Endpoint without a Grant right. This used a combination of `seL4_Send` and `seL4_Wait` to communicate without the ability for capability transfer, however this only supports a single sender and single receiver. - Better support for configuring components with a provided devicetree. This support includes adding a seL4DTBHardware connector that can be used instead of seL4HardwareMMIO and seL4HardwareInterrupt and can be used to extract IRQs and MMIO register information out of the devicetree node rather than specifying the info directly. This connector can also be used to access a devicetree within a component at for querying further device information. There is also a connector seL4VMDTBPassthrough that can be used for specifying devices to pass through to a `camkes-arm-vm` VM component. - CapDL Refinement framework. These are generated Isabelle proof scripts to prove that the generated capDL respects the isolation properties expected from its CAmkES system specification. Only the AARCH32 platform is supported. The generated capDL is a specification of seL4 objects and capabilities that will implement the CAmkES system specification. This specification is then given to a system initialiser to create the objects and capabilities and load the system. - Support for RISC-V systems. ## capDL capDL refers to the capability distribution language and tools contained in https://github.com/seL4/capdl. CAmkES uses these tools for generating a capDL specification and then uses the `capdl-loader-app` as it's seL4 root task for initialising the system. As we are in the process of developing additional loaders we are going to start providing versioned releases of the capDL set of tools. Changes since the last seL4 release: - Support for the new seL4 Endpoint GrantReply access rights in the CapDL spec. Endpoint capabilities in the capDL spec can now have Read, Write, Grant and GrantReply rights. - Static Untyped allocation of spec objects. This is support for performing offline pre-allocation of spec objects to the Untyped objects that are expected to be provided in the seL4_BootInfo by the kernel. Having a static allocation of spec objects to Untypeds allows for more simple loaders that do not have to perform resource allocation during initialisation. This feature is optional and a spec is still valid if objects aren't allocated from Untyped objects. - Support for loading RISC-V systems.

1 0

CAmkES languages
by Michael Neises 21 Oct '19

21 Oct '19

Hi, I have an application written in CakeML that I would like to include in a CAmkES component, but all the documentation I can find only uses C code. Is it possible to use a non-C language as source for a CAmkES component? If so, how can I accomplish this? Best, Michael Neises

2 1

Zynq UltraScale+ locks up after hours running
by Leonid Meyerovich 05 Oct '19

05 Oct '19

Hello, We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102 board). The implementation includes multiple processes, hypervisor and virtual machine running on dedicated core. After several hours running (it could be 2 or even 8 hours) the whole microkernel locks up. After some investigation I have found that no interrupts generated anymore - at least there is no interrupts coming to ISR. Inside ISR I have monitored PL2 Physical Timer Control register, which feeds a scheduler and didn't find any problems - it stays enabled and not masked. I will appreciate any idea/direction for approaching this problem. Thank you, Leonid ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

5 24

Re: [seL4] [Non-DoD Source] Devel Digest, Vol 65, Issue 5
by Seeberger, John T CIV USN NAS PAX MD (USA) 05 Oct '19

05 Oct '19

I have noticed this also. Thad ________________________________________ From: Devel [devel-bounces(a)sel4.systems] on behalf of devel-request(a)sel4.systems [devel-request(a)sel4.systems] Sent: Thursday, October 03, 2019 8:24 AM To: devel(a)sel4.systems Subject: [Non-DoD Source] Devel Digest, Vol 65, Issue 5 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: Zynq UltraScale+ locks up after hours running (Shen, Yanyan (Data61, Kensington NSW)) 2. Re: How to use sel4runtime (Millar, Curtis (Data61, Kensington NSW)) 3. Re: Zynq UltraScale+ locks up after hours running (Leonid Meyerovich) ---------------------------------------------------------------------- Message: 1 Date: Thu, 3 Oct 2019 06:43:52 +0000 From: "Shen, Yanyan (Data61, Kensington NSW)" <Yanyan.Shen(a)data61.csiro.au> To: "lmeyerovich(a)i-a-i.com" <lmeyerovich(a)i-a-i.com>, "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running Message-ID: <78ebf24ad9274ca75e18b5fca8575a09bc423b82.camel(a)data61.csiro.au> Content-Type: text/plain; charset="utf-8" Hi Leonid, Could you provide a bit more about your software configuration? For instance, do you have multiple VMs running on dedicated hardware cores? How are the VM and processes configured? Also, you mean there were no interrupts at all on all the four cores? Regards, Yanyan On Wed, 2019-10-02 at 16:01 +0000, Leonid Meyerovich wrote: > Hello, > > We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102 > board). The implementation includes multiple processes, hypervisor > and virtual machine running on dedicated core. After several hours > running (it could be 2 or even 8 hours) the whole microkernel locks > up. After some investigation I have found that no interrupts > generated anymore - at least there is no interrupts coming to ISR. > Inside ISR I have monitored PL2 Physical Timer Control register, > which feeds a scheduler and didn't find any problems - it stays > enabled and not masked. > > I will appreciate any idea/direction for approaching this problem. > > Thank you, > > Leonid > > > > > This message and all attachments are PRIVATE, and contain information > that is PROPRIETARY to Intelligent Automation, Inc. You are not > authorized to transmit or otherwise disclose this message or any > attachments to any third party whatsoever without the express written > consent of Intelligent Automation, Inc. If you received this message > in error or you are not willing to view this message or any > attachments on a confidential basis, please immediately delete this > email and any attachments and notify Intelligent Automation, Inc. > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel ------------------------------ Message: 2 Date: Thu, 3 Oct 2019 07:04:41 +0000 From: "Millar, Curtis (Data61, Kensington NSW)" <Curtis.Millar(a)data61.csiro.au> To: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How to use sel4runtime Message-ID: <ad55f3a5de7838e0f9d16a94905647a0ead42249.camel(a)data61.csiro.au> Content-Type: text/plain; charset="utf-8" Hi Baltazar, > Another (less exclusively RISC-V related, though I am targeting RISC-V > still) question - I've been trying to figure out the sel4runtime repo, > but I'm a bit confused on how to set it up. Specifically: > > * How much of a "minimal seL4 environment" do I need to initialize > first? The sel4runtime is a minimal C runtime specifically for seL4. It handles the initialization of all applications (root servers and System-V ELF processes) on an seL4 system. A minimal project will require a repo project containing seL4, seL4_tools, musl, and sel4runtime (along with a root task application). sel4runtime is then used as the C runtime for all applications built in the project and is responsible for providing the entrypoints and calling into the main function. > * Do does my program with main() also need to specify a root task, or > is that part of the minimal environment? You will still need to provide a root task application. sel4runtime is only responsible for handling process startup for C applications. > * Is there a specific recommended location for the sel4runtime repo? The sel4runtime repo is usually placed in the projects directory. You can see sel4-tutorials-manifest[^1] repository on github for an example of how the dependecies are laid out. [^1]: https://github.com/SEL4PROJ/sel4-tutorials-manifest Cheers, Curtis Millar Systems Engineer, Trustworthy Systems, CSIRO's Data61 curtis.millar(a)data61.csiro.au Data61, CSIRO Level 3, K17 Building UNSW Gate 14, Barker St Kensington NSW 2033 Australia

2 1

[FOSDEM] [Fwd: CfP: FOSDEM 2020 - Microkernels and Component-based OS devroom] (fwd)
by Stefan Kalkowski 04 Oct '19

04 Oct '19

Hello sel4 community, I think below announcement might be interesting for you too. Best regards Stefan Kalkowski -------- Forwarded Message -------- From: Julian Stecklina <js(a)alien8.de> Reply-To: microkernel-devroom(a)lists.fosdem.org To: l4-hackers(a)os.inf.tu-dresden.de, users(a)lists.genode.org, microkernel-devroom(a)lists.fosdem.org, ukvly-announce(a)freelists.org, helenos-devel(a)lists.modry.cz Subject: CfP: FOSDEM 2020 - Microkernels and Component-based OS devroom Date: Fri, 04 Oct 2019 00:38:35 +0200 [Resent due to wrong Reply-To: header] FOSDEM 2020 - Microkernels and Component-based OS devroom CALL FOR PARTICIPATION The developers of several free and open-source microkernel-based operating systems will meet at FOSDEM 2020 [1] in Brussels, Belgium and will share a developer room. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-, unikernel-, and component-based operating systems. Possible topics include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * used languages and tools * enabling support for hardware (architectures, device drivers) * enabling support for programming languages * maintenance and testing * security and robustness * trends and challenges * use cases, experiences, lessons learned and demos The deadline for your proposal is on December 1, 2019. Please use the Pentabarf [2] system to submit your proposals. You do not need to create a new account if you already have one. Make sure to include the following in your proposal: * title of your talk (will be printed in the FOSDEM booklet) * your full name (will be printed in the FOSDEM booklet) * a short abstract (one or two paragraphs) * duration of your talk (at least 25 and no longer than 55 min) The official devroom schedule (along with the accepted talks) will be announced on December 15 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM website. You are invited to send any other suggestions for what you want to see or do at the devroom to the list. We will also use this list to organize the traditional devroom dinner that will happen on the first day of FOSDEM. About the devroom Since the first Microkernel devroom at FOSDEM 2012, this devroom has been part of each following FOSDEM. The focus gradually widened to include component-based operating systems. By now it has become a somewhat institutionalized tradition for the community to meet there; to this date over a dozen projects have participated in one way or another. Each of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Social events It also has become a habit that the microkernel projects dine together somewhere in Brussels. The year 2020 will not be any different, so there is going to be a dinner on Saturday night. We try place a reservation, so we will inform you about the exact location and time later. Consult the FOSDEM web and other projects for additional social events such as the famous FOSDEM-organized Friday Beer Event and the FOSDEM-arranged free sightseeing tours for spouses. About FOSDEM FOSDEM is a two-day event organised by volunteers to promote the widespread use of free and open source software. Taking place in the beautiful city of Brussels (Belgium), FOSDEM is widely recognised as the best such conference in Europe. FOSDEM covers a wide spectrum of free and open source software projects, and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) with network/internet connectivity and projectors where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and discussions. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. Every year, FOSDEM hosts more than 5000 developers at the ULB Solbosch campus. Participation and attendance is totally free, though the organisers gratefully accept donations and sponsorship. No registration necessary. Important dates recap * 2019-12-01: Deadline for submissions * 2019-12-15: Schedule published and speakers notified of acceptance * 2020-02-01: Devroom Dinner (details to be announced) * 2020-02-01/2020-02-02: The devroom takes places (check the schedule) Links [1] https://fosdem.org/ [2] https://penta.fosdem.org/submission/FOSDEM20 [3] https://lists.fosdem.org/listinfo/microkernel-devroom _______________________________________________ FOSDEM mailing list FOSDEM(a)lists.fosdem.org https://lists.fosdem.org/listinfo/fosdem ----- End forwarded message ----- -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

1 0

Re: [seL4] CapDL output to isabelle file
by Lim, Japheth (Data61, Kensington NSW) 03 Oct '19

03 Oct '19

Hi Norrathep, Norrathep Rattanavipanon wrote: > I have been trying to generate Isabelle file from CapDL specification. But > I run into an error when I'm running the command: > > ./parse-capDL --isabelle=out.thy --object-sizes=object_sizes.yaml > example-arm.cdl > We recently put in a major change to the Isabelle translator. The input capDL file is now required to be pre-allocated, i.e. every object must be placed in an untyped with a known physical address. The existing example files date from before this change, and so they don't meet the requirements to be translated into Isabelle. Sorry that you got confusing error messages as a result. We plan to make this more consistent in the near future. > Is there any step I'm missing? Or does the tool not support the conversion > to Isabelle? The standard way is to build a CAmkES application with the option `CAmkESCapDLStaticAlloc` enabled. This will generate a suitable capDL file for proofs. Based on your other question thread, you may be interested in our README for CAmkES proofs: https://github.com/seL4/camkes-tool/tree/master/cdl-refine-tests This generates proofs between the CAmkES high-level model and the capDL system representation. However, we are not working on C glue code proofs at the moment. This is all work in progress, and quite rough around the edges. Nevertheless, we're happy to try to answer any questions you might have. It would help if we knew more about your work, so that we can give more specific replies. Cheers, Japheth Lim Proof Engineer, Trustworthy Systems

3 5

Initialising Camkes App before another dependent Camkes app
by yogidk . 03 Oct '19

03 Oct '19

Hi, I have a Camkes app (app1) which depends on another Camkes app (app2), which means my app1 must start only after app2 is completely initialized. For this currently I use a signal RPC wait in app1 and the corresponding RPC emit from app2 after app2 is completely initialized. Is there any other way in CamkES which will ensure that app1 starts only after app2 is completely initialized without using RPC signalling (emit and wait) ? How can this dependency be built ? Regards yk

3 2

Re: [seL4] How to use sel4runtime
by Millar, Curtis (Data61, Kensington NSW) 03 Oct '19

03 Oct '19

Hi Baltazar, > Another (less exclusively RISC-V related, though I am targeting RISC-V > still) question - I've been trying to figure out the sel4runtime repo, > but I'm a bit confused on how to set it up. Specifically: > > * How much of a "minimal seL4 environment" do I need to initialize > first? The sel4runtime is a minimal C runtime specifically for seL4. It handles the initialization of all applications (root servers and System-V ELF processes) on an seL4 system. A minimal project will require a repo project containing seL4, seL4_tools, musl, and sel4runtime (along with a root task application). sel4runtime is then used as the C runtime for all applications built in the project and is responsible for providing the entrypoints and calling into the main function. > * Do does my program with main() also need to specify a root task, or > is that part of the minimal environment? You will still need to provide a root task application. sel4runtime is only responsible for handling process startup for C applications. > * Is there a specific recommended location for the sel4runtime repo? The sel4runtime repo is usually placed in the projects directory. You can see sel4-tutorials-manifest[^1] repository on github for an example of how the dependecies are laid out. [^1]: https://github.com/SEL4PROJ/sel4-tutorials-manifest Cheers, Curtis Millar Systems Engineer, Trustworthy Systems, CSIRO's Data61 curtis.millar(a)data61.csiro.au Data61, CSIRO Level 3, K17 Building UNSW Gate 14, Barker St Kensington NSW 2033 Australia

1 0

Run VM guest on seL4 using CAmkEs
by Khalid Amen 03 Oct '19

03 Oct '19

Hello, I am trying to run VM guest on seL4 using CAmkEs. I have setup my linux machine and installed dependencies. I have run seL4 hello world example. What do I need to do run VM guest in seL4? I have serached online to see. The documentation says that to create VM guests and applications on seL4, I need to use CAmkES. I followed this link: https://docs.sel4.systems/Tutorials/camkes-vm-linux.html. What do I need to create VM on top of seL4 using CAmkES? Also, I want seL4 to run as hypervisor. I have found a tutorial on how to run it from these links. https://github.com/seL4/camkes-vm-examples/blob/master/README.md https://docs.sel4.systems/Tutorials/camkes-vm-linux But, I did not understand the following: You can boot the tutorial on an x86 hardware platform with a multiboot boot loader, or use the QEMU <https://www.qemu.org/> simulator. *Note if you are using QEMU it is important to ensure that your host machine has VT-x support and KVM <https://www.linux-kvm.org/page/Main_Page> installed. You also need to ensure you have enabled nested virtulisation with KVM guests as described here <https://www.linux-kvm.org/page/Nested_Guests>.* After building is completed with ninja, how do I excute the following: Then boot images/kernel-x86_64-pc99 and images/capdl-loader-experimental-image-x86_64-pc99 (or *.ia32-pc99 if built for 32-bit) with the multiboot boot loader of your choice. -- Regards, Khalid Ameen

2 1