- Devel - lists.sel4.systems

Reminder seL4 developer hangout
by Birgit Brecknell 07 Aug '23

07 Aug '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Aug 9, 8am For your time zone, please see the 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 2pm-5pm Fri 9am-5pm

1 0

Ultra96V2 in sel4cp_VMM is cautiously here - initial support
by Nataliya Korovkina 06 Aug '23

06 Aug '23

Highlights, briefly... 1. Project "ultra96v2-sel4cpvmm" The project introduces changes to the three components: seL4, sel4CP, sel4cp_VMM. * Xilinx Linux booting requires SMC calls support in seL4. The project uses the SMC cap impelementation offered by DornerWorks (approved but not merged). * Changes in sel4CP relate to the new capability in seL4. * As for sel4cp_VMM, a policy of VM's SMC calls handling will be different from one VMM-PD to another. The project introduces registration of a custom handler by PD application as well as it provides the default handler - the simplest "pipe" passing calls and responses through. The project published as sets of patches to the components. More the details are in the README.md and Issue #1 - https://github.com/malus-brandywine/ultra96v2_sel4cpvmm/issues/1 of the project: https://github.com/malus-brandywine/ultra96v2_sel4cpvmm 2. Project "petalinux-ultra96v2-sel4cpvmm" The project enables generation of linux image and minimal rootfs to run VM with sel4cp_VMM. More details are in README.md of the project: https://github.com/malus-brandywine/petalinux-ultra96v2-sel4cpvmm Status: Linux VM loads to login prompt

1 0

2 weeks left to get the early-bird registration at the seL4 summit
by Birgit Brecknell 04 Aug '23

04 Aug '23

2 weeks left to get the early-bird registration at the seL4 summit! A friendly reminder that the early bird cut-off date is 18 August 2023. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and Dinner Registrations: https://events.linuxfoundation.org/sel4-summit/register/ seL4 summit 2023: https://sel4.systems/Foundation/Summit/2023/<https://sel4.systems/Foundation/Summit/2023/> --- 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 2pm-5pm Fri 9am-5pm

1 0

CMake error “Variable 'KernelArch' is not set.” Happens when building RISCV based seL4 system.
by sueboxian＠gmail.com 25 Jul '23

25 Jul '23

Hi, I met a CMake error, “Variable KernelArch is not set” when I tried to build a seL4 project based on the open source code of the UNSW course, Advanced Operating System, aka. AOS. The original version uses odroidc2 as the building platform, and I want to build it with the riscv gnu toolchain and simulate it on qemu-riscv-virt. Here is the repository: https://github.com/SEL4PROJ/AOS-manifest The building hierachy is as the basic build system structure, with init-build.sh, setting.cmake and CMakeLists.txt in the top level. And the top level contains kernel, tools, and project folders, in which there are CMakeLists.txt and .cmake files. Since I have no experience on cmake, I tried to compare the manifest xml between AOS project and seL4test project. I found that the major difference between them are in “init-build.sh”, “setting.cmake” and the “CMakeList.txt” in the top level. There are also some unused libraries in AOS project. I tried deleting the “set PLATFORM odroidc2” command in the setting.cmake, and added the DCROSSCOMPILER=riscv-unknown-linux-gnu, DPLATFORM=qemu-riscv-virt in the build command. But they doesn’t work. After checking the “/kernel/configs/seL4Config.cmake”, it says that the error is caused since KernelArch is left as empty string… And I want to ask whether I have set anything improperly.... I will appreciate for any help. Thank you for reading my question!

3 2

Reminder seL4 developer hangout
by Birgit Brecknell 24 Jul '23

24 Jul '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Jul 26, 5pm For your time zone, please see the 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 2pm-5pm Fri 9am-5pm

1 0

Soft-float problem happens when building seL4test using riscv64-unknown-linux-gnu-gcc toolchain
by sueboxian＠gmail.com 15 Jul '23

15 Jul '23

Hi, I met a problem when building seL4test project with riscv toolchain, with the float operations compiled as soft-float. Here are my configuration commands:  python3 ~/bin/repo init -u https://github.com/seL4/sel4test-manifest  python3 ~/bin/repo sync  mkdir build-riscv  cd build-riscv  ../init-build.sh -DPLATFORM=qemu-riscv-virt -DCROSS_COMPILER_PREFIX=riscv64-unknown-linux-gnu- -DSIMULATION=TRUE  ninja The terminal reported "can't link double-float modules with soft-float modules" errors when compiling fpu.c, and thus stopped compilation. I have tried rebuilding the glibc version riscv toolchain, with multilib enabled. But it doesn't work. I also checked the terminal, it says that I'm compiling with march=riscv64imac_zicsr_zifencei -mabi=lp64, which as the best of my knowledge, means compiling the float as soft-float. I want to know whether I lossed something. I would appreciate for any help. Thanks in advance.

3 6

Reminder seL4 developer hangout
by Birgit Brecknell 10 Jul '23

10 Jul '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Jul 12, 8am For your time zone, please see the 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 2pm-5pm Fri 9am-5pm

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 23 Jun '23

23 Jun '23

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

1 0

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

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