July 2022 - 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 that this method not implemented yet so i return 0 in this method and resolved. for second problem that cause failure if trace program and i found that in "init rumprun" process the program failed in the /projects/sel4runtime/include/sel4_arch/x86_64/sel4runtime/thread_arch.h file and sel4runtime_set_tls_base method. so i read git log and in recently commit your team use sel4runtime for thread TLS, so when we run rumprun_hello, the program failed in sel4runtime_set_tls_base method. can you help me fix this bug? thanks for your attention. -- This email was Anti Virus checked by Security Gateway.

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 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 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 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

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

Proper seL4 APi/ABI design
by Eric Jacobs 17 Sep '22

17 Sep '22

Jumping off from the recent thread, I was curious if anyone had any thoughts about how to optimally design API's for seL4. I noticed we had a bit of info about what not to do (don't do long IPC, don't implement Posix, don't use messaging as synchronization, etc.) Are there any shining examples of what _to_ do with an API? Thanks, -Eric

5 11

Thread Scheduling Domains
by June Tate-Gans (ジューン) 02 Aug '22

02 Aug '22

Hey folks, So Sam and I are at the point now where we're attempting to get our untrusted user threads running in a different scheduling domain, and it's not exactly clear how this is supposed to work in terms of enabling more than one domain in the kernel. So far, I've set KernelNumDomains to 2 in the easy-settings.cmake for our project, but unless I provide a separate implementation of kernel/config/default_domain.c by overriding KernelDomainSchedule, the resulting kernel will only think it has one domain and only ever schedule domain 0 for execution. Are we expected to override the default_domain.c file with our own in the project, like sel4test seems to do? Thanks! -- June Tate-Gans Software Engineer

2 5

Reminder seL4 developer hangout
by Birgit Brecknell 25 Jul '22

25 Jul '22

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Wed, Jul 27, 7am (UTC), Topics: (open) * Sydney: Wed, Jul 27, 5pm * Central Europe: Wed, Jul 27, 9am * US Pacific Time: Wed, Jul 27, 12 midnight * Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 1

Sydney get-together on seL4 Day?
by Gernot Heiser 20 Jul '22

20 Jul '22

This is only of interest for those physically in Sydney. We have seL4 Day coming up (29 July, the 13th anniversary of completion of the seL4 verification and 8th anniversary of its open-sourcing). It would be great to use the occasion to get together. The continuing abnormal (i.e. very wet) weather in Sydney makes planning such an event difficult (and I’ll be on leave and out of town until the evening of the 28th), so things may have to happen on short notice. But weather permitting, a BYO BBQ in Maroubra would be great, and I would really love to catch up with the rest of the Sydney-based seL4 community. So I suggest people interested save the date (and let us know if you’re interested). Gernot

1 0

suggestion; update faq reference to ODROID-C2
by Van Ly 18 Jul '22

18 Jul '22

Hello, The faq section on "How can I build a system with seL4?" [1] has an obsoleted/discountinued product pointing to ODROID-C2 [2] a current product such as the one from OnLogic can replace, perhaps. [3] ``` If you have access to an Odroid-C2, you should be able to do the project work yourself as a way of familiarising yourself with seL4. ``` [1] https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html [2] https://www.hardkernel.com/shop/odroid-c2/ [3] https://www.onlogic.com/industrial-raspberry-pi/ -- vl

6 7

Systems with multiple PCI root complexes
by Peter Chubb 18 Jul '22

18 Jul '22

Has anyone extended the code in https://github.com/seL4/util_libs libpci to handle multiple root complexes? See bug https://github.com/seL4/util_libs/issues/131 I know genode added code to handle this, but they don't use that library. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW

1 0