August 2024 - Devel - lists.sel4.systems

hello_rumprun app not worked
by MOHAMAD REZA SHAFIEI 19 Apr '25

19 Apr '25

hi. i'm recently worked on sel4 with camkes framework. when i compile rumprun_hello on x86_64 platform its compiled and build correctly but when run with qemu by ./simulate script, program crashed with this errors: simple_get_extended_bootinfo_length@simple.h:600 simple_get_extended_bootinfo_length not implemented FAULT HANDLER: data fault from hello.hello_0_control (ID 0x1) on address 0x8, pc = 0x402b7f, fsr = 0x6 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x402b7f , . . so i found … [View More]

5 5

seL4 test on x86
by Yevgeny Lavrov 30 Jan '25

30 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling … [View More]

4 3

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 16 Oct '24

16 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating … [View More]

3 4

seL4 developer hangout reminder
by Birgit Brecknell 19 Aug '24

19 Aug '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 21 Aug, 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

Gpu passthrough
by Hugo V.C. 15 Aug '24

15 Aug '24

Hi all, here a simple question: is there any example/tutorial off gpu passthrough to a Linux guest? Best,

4 6

Build failure for sel4 on raspberry pi 5
by l4＠photiczone.com 14 Aug '24

14 Aug '24

Hi everyone, I am getting a link failure during the build of sel4test-tests: /usr/bin/ld: apps/sel4test-driver/musllibc/build-temp/stage/lib/libc.a(__stdio_exit.o): copy relocation against non-copyable protected symbol `__stdin_used' collect2: error: ld returned 1 exit status Searching t'interwebs seems to imply this is a gnarly problem caused by the nuances of various build tools - but one that should not apply to Arm. You can summarise everything I did before the build like this: sudo … [View More]

3 4

I am interested in porting LionOS to X64 architecture
by Peter Relich 14 Aug '24

14 Aug '24

Hello, I am a researcher at Intellisense Systems, Inc. We are a small business that performs R&D for the U.S. Military. We have an active contractor to build a hypervisor for a microkernel. We recently selected Sel4 as the microkernel and I learned that the Army (our customer) used a camKes implementation of a VMM to host a fork of Ubuntu, but the limitations prompted them to try another approach. I think since that time, microkit has developed quite a bit and I saw the trustworthy systems … [View More]

5 5

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(… [View More]

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 … [View More]

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