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 …
[View More]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
[View Less]
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 …
[View More]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
[View Less]
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>
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 …
[View More]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
[View Less]
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>
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 …
[View More]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.
[View Less]
Hello!
I recall reading about old CPUs/ISAs made for Lisp machines, with features and optimized for specifically running Lisp. And I’ve heard people discuss how current CPUs are optimized for C code and similar programming paradigms, and vice versa: C and others are optimized for those CPUs.
This got me wondering, what might a CPU or instruction set designed more specifically to run seL4 look like? I’m guessing it might involve capability hardware like CHERI to accelerate seL4’s software …
[View More]implementation of capabilities, but what else might be relevant?
Thanks,
Isaac Beckett
[View Less]
