- Devel - lists.sel4.systems

MCS round-robin scheduling not behaving as expected
by liam.vervecken＠gmail.com 12 Aug '24

12 Aug '24

Hello, I'm trying to understand MCS and how the scheduling works but I'm running into some issues. My setup: RISCV on BeagleVFire in sel4test I have configured 2 threads: seL4_SchedControl_ConfigureFlags(info->schedcontrol.start, sched_context_thread2, 1000000, 1000000, 0, 0, 0); seL4_SchedContext_Bind(sched_context_thread2, thread2_TCB); seL4_SchedControl_ConfigureFlags(info->schedcontrol.start, sched_context_thread3, 1000000, 1000000, 0, 0, 0); seL4_SchedContext_Bind(sched_context_thread3, thread3_TCB); The threads have the same priority. From the documentation I was expecting them to behave like this: - Thread1 does something - Thread2 does something - Thread1 does something - ... But it seems instead only the first thread gets scheduled, and it never allows the second thread to get any CPU time. Am I correct in assuming that 2 threads with period=budget and equal priority should be scheduled round-robin? I found that if I call seL4_SchedContext_Consumed(sched_context_thread) periodically in the threads they will switch if the budget has expired. It doesn't make much sense to me why this is the case, I thought they would switch automatically once their budget is expired and that seL4_SchedContext_Consumed() was simply used to keep track of this. I'm hoping it can offer some clue as to what I'm doing wrong. Any help or guidance would be greatly appreciated. Kind Regards, Liam

6 6

LionsOS as basis for mobile/handheld OS
by Isaac Beckett 10 Aug '24

10 Aug '24

I was looking at LionsOS docs recently, and noted it is meant for static systems with no support for changing hardware at runtime. This is less of a problem for phones and other handhelds given they generally keep the same hardware throughout their service life, but I was concerned about peripheral support. What if I want to be able to connect an external display to a phone or tablet running a LionsOS based userspace? Or I have privacy switches on the device that physically disconnect components such as the modem or camera assembly? Most of the system would be static, and only really changing for things such as loading isolated, untrusted application code (such as a Linux kernel, or something pretending to be a Linux kernel), but it would still have some hardware components that can be disconnected. Though at least in the case of privacy switches they would be the same components every time. What do y’all think? Does this idea of building a mobile phone OS on LionsOS have merit or would it make more sense to use a different framework or build something on seL4 directly?

3 3

LionOS Docs
by Hugo V.C. 09 Aug '24

09 Aug '24

Hi! I'm planning to switch from CAmkES to LionOS but I got a 404 on this link: https://github.com/au-ts/lionsos-docs that is on this URL: https://www.lionsos.org/docs/tutorials/ Best,

2 1

Release 0.2.0 of LionsOS
by Ivan Velickovic 06 Aug '24

06 Aug '24

Hello everyone, There has been a new release of LionsOS, 0.2.0. This release is primarily focused on maturing the existing OS services and making it easier to build LionsOS-based systems. You can find detailed release notes here: https://github.com/au-ts/lionsos/releases/tag/0.2.0 Thanks, Ivan

1 0

Release 0.5.0 of the seL4 Device Driver Framework
by Ivan Velickovic 06 Aug '24

06 Aug '24

Hello everyone, There has been a new release of the seL4 Device Driver Framework, 0.5.0. This release is primarily focused on making the various device classes we support more mature. You can find detailed release notes here: https://github.com/au-ts/sddf/releases/tag/0.5.0 You can find the latest design documentation attached to the release artefacts. Thanks, Ivan

1 0

Release 1.4.0 of Microkit
by Ivan Velickovic 05 Aug '24

05 Aug '24

Hello everyone, We have made a new release of the seL4 Microkit, version 1.4.0. This release contains a number of features requested by the community. You can find the release notes here: https://docs.sel4.systems/releases/microkit/1.4.0 You can find the SDK downloads here: https://github.com/seL4/microkit/releases/tag/1.4.0 Thanks, Ivan

1 0

seL4 developer hangout reminder
by Birgit Brecknell 05 Aug '24

05 Aug '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 6 Aug, 10:00pm UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

How do I reduce the size of the seL4 executable?
by liam.vervecken＠gmail.com 26 Jul '24

26 Jul '24

Hello, I'm trying to compile a simple 'hello world' sel4 program for the polarfire (riscv) and I want the executable to be as small as possible. According to the FAQ (https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html) the single core kernel can compile to a <200kb executable but in my testing, I always end up with an image of approx 2MB. I worked with this (https://github.com/mskordal/SeL4-hello-world) example project and changed main.c to work with seL4_DebugPutChar instead of printf. Besides that, I added opensbi to the tools folder and slightly modified line 32 of projects/hello/CMakeList.txt to target_link_libraries(hello sel4 sel4_autoconf sel4runtime sel4platsupport). After running ../init-build.sh -DPLATFORM=polarfire and ninja, I end up with an executable of about 2MB. I'm guessing musllibc, util_libs and sel4_libs contribute to the size, but if I change my cmakelist file to try to get rid of them the build will fail. I was hoping since my hello world only uses sel4 APIs I could compile it without musllibc, util_libs and sel4_libs but I haven't been able to figure out how. Any help or tips would be greatly appreciated. Kind Regards, Liam

1 0

next seL4 TSC meeting on Thu 25 Jul
by Gerwin Klein 24 Jul '24

24 Jul '24

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Thu, 25 Jul, 4pm - Central Europe: Thu, 25 Jul, 8am - US West Coast (LA/SF): Thu, 25 Jul, 0:00h See also the seL4 calendar feed available from here: https://sel4.systems/contact/home.pml The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/89949317341?pwd=JSC976ciVYmbDJByjSFH0chh78sCsg.1 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - action items from last meeting - discuss new FPU RFC: https://github.com/seL4/rfcs/pull/26 - hear about progress on PMU, budget limit, device driver framework - make decision on old RFC-4: https://github.com/seL4/rfcs/pull/12 - any feedback on GitHub RFC implementation - bump version of cmake-format (will break current formatting) to reduce python dependency hell If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

3 6

seL4 developer hangout reminder
by Birgit Brecknell 22 Jul '24

22 Jul '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 24 Jul, 8:00am UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0