August 2024 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 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 seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

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

15 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 stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

seL4 developer hangout reminder
by Birgit Brecknell 18 Aug '24

18 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 apt install ninja-build libxml2-utils repo pip3 install pyyaml typing hardware pyfdt jinja2 jsonschema six future ply python3-protobuf grpcio-tools cd && mkdir xxx && cd xxx Then to follow your build repo init -u https://github.com/seL4/sel4test-manifest.git repo sync mkdir build && cd build ../init-build.sh -DPLATFORM=bcm2711 ninja And yes I know it is not supported and the BCM2711 is for the Pi 4. I am evaluating ;) Any help greatly appreciated. Thanks, Smiley

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 has even been developing an operating system on the Sel4 microkernel. However, LionOS appears to be developed for ARM systems as the use case. For the Army use, we are using a Nuvo7000LP: https://www.neousys-tech.com/Resource/Product_Document/Nuvo-7000LP/Nuvo-700… Which is an X64 architecture. I just started learning microkit through your available tutorials and I am aware that building a comprehensive VMM is no easy task. However, I was wondering if you had some intuition or if you could provide me an estimate of the libraries in the LionOS that I would need to adjust/redesign to make an X64 architecture fork? Is this even a feasible approach? It looks like I just need to swap out the aarch64 libraries with compatible x64 libraries and do some testing. Before I commit, I just wanted to get some advice on the endeavor. Is forking LionOS to an X64 architecture feasible, or should I start at a lower level (i.e., redesigning the vmm?) Thanks so much for your time. Respectfully, Peter Relich Research Scientist Intellisense Systems, Inc. ________________________________ The information contained in this e-mail and any attachments from Intellisense Systems may contain confidential and/or proprietary information, and is intended only for the named recipient to whom it was originally addressed. If you are not the intended recipient, any disclosure, distribution, or copying of this e-mail or its attachments is strictly prohibited. If you have received this e-mail in error, please notify the sender immediately by return e-mail and permanently delete the e-mail and any attachments.

5 5

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

11 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 09 Aug '24

09 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. 08 Aug '24

08 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