May 2023 - Devel - lists.sel4.systems

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

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

07 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

question about sel4 kernel preemptionPoint
by yadong.li 05 Jun '23

05 Jun '23

Hi: I have one question about sel4 kernel preemptionPoint on smp platform such as ARMv8. Take an example, when kernel takes long time to clear memory when UntypedRetype kernel object on core1, it will check preemptionPoint, when pending IRQ exists on core1, it will handle this irq, and return to userspace let other syscall or cores such as core2 have chance to run, but irq pending only check current cpu(PerCPU), no all cores of smp system, if core1 execute long seL4_Untyped_Retype syscall, core2 has a pending irq, the pending irq will not be checked in current core1, it will block until the execution of long syscall is completed if we take no account of archtimer irq, This phenomenon looks inconsistent at the system level between signal core and mutil core I want to know the current design intent about preemptionPoint of archtimer interrupt and other peripheral interrupts on SMP platform, only take current core interrupt as soon as possible or give other core and high priority task a chance to entry kernel and take big kernel lock? Thanks for your help

2 1

porting to a new platform
by steve.burke.56＠gmail.com 01 Jun '23

01 Jun '23

I'm trying to port an old sel4 code base to the latest so I decided to take the sel4test manifest & work through through the following page (https://docs.sel4.systems/projects/sel4/porting.html) The old code base does not add the new platform the same way since the new code seems to have some new CMake macros that do most of the heavy lifting. Is there a test project that does this with an arbitrary platform that I can use as a reference? My platform defines don't seem to be coming through correctly. Is working through the porting page the best way to do and does it seem current? Thanks.

3 2

Reminder seL4 developer hangout
by Birgit Brecknell 29 May '23

29 May '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, May 31, 7am (UTC), Topics: (open) * Sydney: Wed, May 31, 5pm * Central Europe: Wed, May 31, 9am * US Pacific Time: Wed, May 31, 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

Ring 3 iopl is going away, seL4 is ok
by William ML Leslie 21 May '23

21 May '23

Hello, I just noticed in the new x86-S rfc that Intel published that there will be no further support for io port access for processes in ring 3. Thankfully, this doesn't look like it will impact seL4, which provides capabilities to special objects representing port ranges on x86, which are then implemented in the kernel. Just in case anyone was wondering if there will be any impact, since this is the one thing that stuck out to me. Here's Intel's RFC: https://www.intel.com/content/www/us/en/developer/articles/technical/envisi… I think I might steal your IO port API for newer versions of Coyotos, which /is/ impacted by the change. TBF, I think seL4 has a better IRQ handling interface than the one we currently have too. I guess it's only fair it goes both ways! -- William ML Leslie

3 3

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

Reminder seL4 developer hangout
by Birgit Brecknell 15 May '23

15 May '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, May 16, 10pm (UTC), Topics: (open) * Sydney: Wed, May 17, 8am * Central Europe: Wed, May 17 12pm midnight * US Pacific Time: Tue, May 16, 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

Reminder seL4 developer hangout
by Birgit Brecknell 01 May '23

01 May '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, May 3, 7am (UTC), Topics: (open) * Sydney: Wed, May 3, 5pm * Central Europe: Wed, May 3, 9am * US Pacific Time: Wed, May 3, 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 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0