Devel

devel@sel4.systems

13 participants
1410 discussions

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

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

24 Jul '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

4 3

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

Announcing beta.sel4.systems running on LionsOS
by James Archer 11 Jul '24

11 Jul '24

Trustworthy Systems is now serving a copy of the seL4.systems website from a beta LionsOS-based[1] webserver. It can be accessed at https://beta.sel4.systems/. The source code can be found in the LionsOS repository[2]. More information about the implementation can be found at https://beta.sel4.systems/Info/Website/. Any feedback or attempts to break it are welcome. [1] https://lionsos.org/ [2] https://github.com/au-ts/lionsos James

3 3

seL4_X86_Page_Map on seL4_X86_LargePageObject != 2MiB
by Ben McCart 10 Jul '24

10 Jul '24

I have created my own project on the PC99 architecture (x64) and have been working through the tutorial source (copy & pasted into my project) to learn and then prototype with seL4. I have done the mapping tutorial (pc99) and utilized that code within my project and everything seems to work just fine, but if I change out the seL4_X86_4K to seL4_X86_LargePageObject I don't end up with 2MiB of mappable virtual space. All the seL4 system calls through the client API return seL4_NoError. The seL4_LargePageBits value is 21 (2^21 == 2MB, and intel documentation for IA-32e shows that 2 MiB should be the large page size. However, if I address memory outside of the first 256 KiB it halts. The following works: seL4_Word *x = (seL4_Word *) TEST_VADDR; printf("Read x: %lu\n", *x); And this works: seL4_Word *x = (seL4_Word *) TEST_VADDR + 0x0003FFF0; printf("Read x: %lu\n", *x); But this halts when trying to dereference x to print it: seL4_Word *x = (seL4_Word *) TEST_VADDR + 0x00040000; printf("Read x: %lu\n", *x); I am running seL4 12.1 using QEMU with the following command line: qemu-system-x86_64 -cpu Nehalem,-vme,+pdpe1gb,-fsgsbase,-invpcid,+syscall,+lm,enforce -nographic -serial mon:stdio -m size=512M -s -S -kernel ../sel4-project/build/images/kernel-x86_64-pc99 -initrd build/cxxkit Does anybody have any idea why I might be having this issue and what I may do about it? -Ben McCart

2 2

seL4 developer hangout reminder
by Birgit Brecknell 08 Jul '24

08 Jul '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 9 Jul, 22:00 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

New release of seL4, Microkit, CAmkES, capDL and Rust support
by Gerwin Klein 02 Jul '24

02 Jul '24

We’re pleased to announce the release of - seL4 13.0.0: The seL4 microkernel https://docs.sel4.systems/releases/sel4/13.0.0 - Microkit 1.3.0: The seL4 Microkit for building static-architecture systems https://docs.sel4.systems/releases/microkit/1.3.0 - CAmkES 3.11.0: Component Architecture for microkernel-based Embedded Systems https://docs.sel4.systems/releases/camkes/camkes-3.11.0 - capDL 0.3.0: Tools for generating, parsing and loading capability distribution specifications https://docs.sel4.systems/releases/capdl/0.3.0 - rust-sel4 1.0.0: Rust support for seL4 userspace https://github.com/seL4/rust-sel4/releases/tag/v1.0.0 See https://github.com/seL4/rust-sel4/ for more information. Microkit 1.3.0 and rust-sel4-1.0.0 are the first official releases under the seL4 foundation. Cheers, Gerwin

1 0

New release of seL4, Microkit, CAmkES, capDL and Rust support
by Gerwin Klein 02 Jul '24

02 Jul '24

1 0

seL4 MCS flavour with RISCV
by David Martin 01 Jul '24

01 Jul '24

Hello, I'm trying to understand the current situation of the MCS branch. Our setup: - Microchip Polarfire SoC (1xE51 RV64IMAC + 4xU54 RV64IMAFD) We are starting to "play" with threads but when coming to the scheduling of them, I'm a bit lost. If I understand correctly, the latest version of seL4 (12.1.0) if compatible with RV64IMAFD, so floating point operations included. The latest MCS version (10.1.1-mcs) on the contrary is only RV64IMAC so no FPU support. I haven't seen any MR nor discussion about including that FPU support when using RISCV processors... Am I correct in here? or I am missing something? (It's not really clear to me when I read the docs to be honest) Thanks for your support. - David.

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel