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

iMX8MM seL4 12.1.0 running a VM
by Zippy Manaic 22 Nov '24

22 Nov '24

Hi, I have encountered a problem where the device tree is not correctly being parsed resulting in interrupts not being routed to the VM. A node which exhibits this issue is (there are several more in the iMX8MM device tree that also trigger the problem) ``` snvs@30370000 { compatible = "fsl,sec-v4.0-mon\0syscon\0simple-mfd"; reg = <0x30370000 0x10000>; phandle = <0x1b>; snvs-rtc-lp { compatible = "fsl,sec-v4.0-mon-rtc-lp"; regmap = <0x1b>; offset = <0x34>; interrupts = <0x00 0x13 0x04 0x00 0x14 0x04>; clocks = <0x02 0xe4>; clock-names = "snvs-rtc"; }; }; ``` Interrupts 0x13 and 0x14 should be included in the camkes_dtb_irqs[] variable but they are not. Looking at the node as it is parsed in macros.py via the function parse_dtb_node_interrupts {'compatible': ['fsl,sec-v4.0-mon', 'syscon', 'simple-mfd'], 'reg': [808910848, 65536], 'phandle': [27], 'snvs_rtc_lp': [<pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c28f10>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c28f70>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c28fd0>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f070>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f0d0>, <pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c2f130>], 'snvs_rtc_lp_compatible': ['fsl,sec-v4.0-mon-rtc-lp'], 'snvs_rtc_lp_regmap': [27], 'snvs_rtc_lp_offset': [52], 'snvs_rtc_lp_interrupts': [0, 19, 4, 0, 20, 4], 'snvs_rtc_lp_clocks': [2, 228], 'snvs_rtc_lp_clock_names': ['snvs-rtc'], 'snvs_powerkey': [<pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c2f1f0>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f250>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f2b0>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f310>, <pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c2f370>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f3d0>, <pyfdt.pyfdt.FdtProperty object at 0x7483b4c2f430>, <pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c2f490>], 'snvs_powerkey_compatible': ['fsl,sec-v4.0-pwrkey'], 'snvs_powerkey_regmap': [27], 'snvs_powerkey_interrupts': [0, 4, 4], 'snvs_powerkey_clocks': [2, 228], 'snvs_powerkey_clock_names': ['snvs-pwrkey'], 'snvs_powerkey_linux_keycode': [116], 'snvs_powerkey_wakeup_source': [], 'snvs_powerkey_status': ['okay'], 'this_address_cells': [1], 'this_size_cells': [1], 'this_node_path': '/soc@0/bus@30000000/snvs@30370000'} The function is looking for 'interrupts' but the interrupt declaration in the child node has been renamed to 'snvs_rtc_lp_interrupts'. This explains why the interrupts are omitted from the template generated code. A hacky fix, that does appear to work, is to paste the interrupt declarations into the parent node. I'm sure there's a more elegant way to resolve this but my detailed knowledge in this area is lacking. I am going to have a look at seL4 13.0.0 to see if this has already been fixed with a view to a potential backport but thought I'd check here before starting to dig a new hole to fall into. Many thanks, Zippy

2 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

seL4 developer hangout reminder
by Birgit Brecknell 30 Sep '24

30 Sep '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 1 Oct, 10:00pm 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

General Question On Object Methods
by tunacici7＠gmail.com 25 Sep '24

25 Sep '24

I've recently started to learn seL4 by following the Tutorials, which have been great so far. I've been also reading the Manual & API reference to understand and gain insight into different mechanisms. However, I have one fundamental question: Are the object methods system calls? It is said that seL4 only has 3 logical system calls: Send, Recv and Yield. (In all the slides, videos and other documents I have seen) And the rest is just variations of those ones. But what about object methods? Are they system calls? Are they executed in kernel space? If they are system calls, then wouldn't all the resources out there be misleading? Since there are way more than just Send, Recv and Yield. If they are not, then how are they handled? Does 'libsel4' have anything to do with it? I can't imagine 'seL4_Untype_Retype' executing in user space. Unfortunately, I couldn't find any answers to this question online. So that's why I'm asking it here. Maybe there are others who wonders the same thing. NOTE The API Reference page confuses me even more. It lists Object Methods in its own category (instead of being under System Calls). Does this means Object Methods are NOT system calls? Or the term System Call is just not what I think it is(basically an endpoint to kernel)?. END NOTE Thanks for the answers in advance. -T

8 21

seL4 developer hangout reminder
by Birgit Brecknell 16 Sep '24

16 Sep '24

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

Less than 1 week left to get the early-bird registration for the seL4 summit
by Birgit Brecknell 09 Sep '24

09 Sep '24

Less than 1 week left to get the early-bird registration for the seL4 summit The early bird cut-off date for the seL4 summit 2024 [0] is 15 September 2024. The summit will be held in Sydney, Australia, 15-17 October 2024. The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and dinner Register here [1] A number of informal social activities [2] are being organised by local Sydney-siders. Check out the list [2] and contact the organiser to register your interest. [0] https://sel4.systems/Foundation/Summit/2024/ [1] https://events.linuxfoundation.org/sel4-summit/register/ [2] https://sel4.systems/Foundation/Summit/2024/social-activities 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

Virtual address ranges used in seL4 initial thread after boot?
by Ben McCart 06 Sep '24

06 Sep '24

I have read the manual in section 9.2 about userImageFrames and how to infer the virtual address range for the pages being used for the userland image, which I frankly do not concretely understand. For example, I can take the address of main() and that leads me to believe my first user image frame (page frame actually I suspect) is probably at 0x40000, but it feels like guessing. (Not good!) In addition, I like to know the address range used for the stack of the initial thread, as well as any other reserved regions (I read somewhere in the manual about reserved virtual address space for the kernel, but I can't remember where I read that and now I can't find it.) Are there any macros included in public header files that I can use in my project to get the starting addresses for any of these regions? Barring that, is there any straight-forward reliable way to find the starting address for these regions (or in the case of kernel reserved virtual address range is it documented anywhere?) I am on version 12.0 of seL4 for my project. Thank you! -Ben

2 2

Less than 2 weeks left to get the early-bird registration for the seL4 summit
by Birgit Brecknell 02 Sep '24

02 Sep '24

Less than 2 weeks left to get the early-bird registration for the seL4 summit The early bird cut-off date for the seL4 summit 2024 [0] is 15 September 2024. The summit will be held in Sydney, Australia, 15-17 October 2024. The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and dinner Register here [1] A number of informal social activities [2] are being organised by local Sydney-siders. Check out the list [2] and contact the organiser to register your interest. [0] https://sel4.systems/Foundation/Summit/2024/ [1] https://events.linuxfoundation.org/sel4-summit/register/ [2] https://sel4.systems/Foundation/Summit/2024/social-activities 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

seL4 developer hangout reminder
by Birgit Brecknell 02 Sep '24

02 Sep '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 3 Sep, 10:00pm 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