April 2023 - Devel - lists.sel4.systems

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

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

Bitfield generator EBNF grammar
by June Tate-Gans (ジューン) 06 Jun '23

06 Jun '23

Hey guys, I've been attempting to put together some rust bindings for the seL4 fault handling mechanisms, and I'm afraid the bitfield generator is driving me a bit up a wall at this point. I'd like to find a concise grammar for the language so I can better understand how bitfield_gen.py works, but there doesn't seem to be any explicit BNF for it anywhere. Is there a paper I should be reading or a reference guide somewhere that would help? Thanks! -- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Google

3 5

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

18 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

One week to go to submit a talk for seL4 summit 2023!
by Birgit Brecknell 17 Apr '23

17 Apr '23

One week to go to submit a talk for seL4 summit 2023 [0]! If you'd like to submit a talk, please upload an abstract of one page or less to the submission portal [1]. The seL4 Summit 2023 will be held 19 - 21 September 2023 at the Elliot Park Hotel, Minneapolis, USA. The summit will be hosted by the Linux Foundation, and will be an in-person event. Registration details to follow soon. We're looking forward to many exciting proposals! [0] https://sel4.systems/Foundation/Summit/2023/cfp [1] https://sel4.systems/Foundation/Summit/2023/submit --- 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 0

Reminder seL4 developer hangout
by Birgit Brecknell 17 Apr '23

17 Apr '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Apr 18, 10pm (UTC), Topics: (open) * Sydney: Wed, Apr 19, 8am * Central Europe: Wed, Apr 19, 12pm midnight * US Pacific Time: Tue, Apr 18, 3pm Calendar link: https://sel4.systems/contact/ 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 0

Release of the CAmkES to seL4CP Transition Guide
by Jingyao Zhou 13 Apr '23

13 Apr '23

Hi all, The initial version of the CAmkES to seL4CP Transition Guide has been released. The guide aims to provide information and advice for those who are migrating applications built using CAmkES to the seL4 Core Platform. The main focus of this guide is on device driver development and virtual machine (monitor) development. The PDF version of this guide can be found on the Trustworthy Systems web page: https://stage.trustworthy.systems/projects/TS/sel4cp/2304-11-camkes-to-sel4… <https://stage.trustworthy.systems/projects/TS/sel4cp/2304-11-camkes-to-sel4…> The source of this guide can be found in the Trustworthy Systems GitHub repository: https://github.com/au-ts/camkes_to_sel4cp_guide <https://github.com/au-ts/camkes_to_sel4cp_guide> Please don’t hesitate to provide feedback! Regards, Jade.

2 4

Reminder seL4 developer hangout
by Birgit Brecknell 03 Apr '23

03 Apr '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Apr 5, 7am (UTC), Topics: (open) * Sydney: Wed, Apr 5, 5pm * Central Europe: Wed, Apr 5, 9am * US Pacific Time: Wed, Apr 5, 12pm (midnight) Calendar: https://sel4.systems/contact/ 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 0