February 2022 - Devel - lists.sel4.systems

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

libsel4muslcsys: Error attempting syscall 215
by skydivebcn＠gmail.com 05 Mar '22

05 Mar '22

Hi guys, I was trying to boot a custom Linux 4.9.302 Kernel and fot this horrible message: "libsel4muslcsys: Error attempting syscall 215" hugo@dev:~/seL4/sel4webserver_hugusmaximus_fork/build$ sudo ./simulate --extra-qemu-args="-netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01,disable-modern=on,disable-legacy=off" [sudo] contraseña para hugo: ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01,disable-modern=on,disable-legacy=off -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61bf9000..631120af] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61d3a2b8. Loaded DTB from 61d3a2b8. paddr=[60243000..60244fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60242fff] vaddr=[ff8060000000..ff8060242fff] virt_entry=ff8060000000 ELF-loading image 'capdl-loader' to 60245000 paddr=[60245000..617fdfff] vaddr=[400000..19b8fff] virt_entry=408f38 Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/205 T0xff80bf815400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> Loading Linux: 'linux' dtb: 'linux-dtb' install_linux_devices@main.c:655 module name: map_frame_hack install_linux_devices@main.c:655 module name: init_ram install_linux_devices@main.c:655 module name: cross_vm_connections libsel4muslcsys: Error attempting syscall 215 libsel4muslcsys: Error attempting syscall 215 _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0x8020000 as this is purely an seL4 error message (musl libc seL4 code?) then I would appreciate any hint about what can be going on. P.S.: I have run my seL4 qemu aarch64 with several Linux kernel versions and never had this problem until now.

2 1

Call for support contract to the seL4 Foundation
by Birgit Brecknell 25 Feb '22

25 Feb '22

A friendly reminder that bids are due before March 4th, 2022 AOE: The seL4 foundation is seeking to contract support for the following duties: - address open github issues in the seL4 organisation repositories, with prioritisation directed by the TSC delegates; this includes: - documentation, tutorials - bugs - tests - docsite and possibly website in coordination with Foundation people - help keeping an eye on making sure questions on mailing lists, discourse and github issues are answered (by someone) Requirement for the person working on these tasks are: - multiple years of experience with seL4, both at kernel level and user-level code - good familiarity with the seL4 organisation repositories - active contributor to one or more seL4 repositories - fluent in written and spoken English The seL4 foundation would contract a service company, initially for 6 months. The service company should identify the person that will be performing the work, ideally on a full-time basis. To bid for the contract, send email to foundation(a)sel4.systems before March 4th, 2022 AOE, with the resume of the person that will be performing the work and a cover letter addressing the requirements. --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au seL4 Foundation, birgit(a)sel4.systems 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Re: Announcing Neptune OS release v0.1.1: A Windows NT personality for seL4
by Chang Liu 24 Feb '22

24 Feb '22

Thank you both for the discussion on licensing. Seems that GPLv3 is a good choice for now. Wikipedia seems to claim that ReactOS is licensed under "GPLv2 or any later version" but I didn't find this on the reactos source code itself. If the ReactOS foundation has an objection later I can always change it to v2. Best, Chang On Wed, Feb 23, 2022 at 12:09 AM G. Branden Robinson < g.branden.robinson(a)gmail.com> wrote: > Hi Chamg, > > At 2022-02-22T23:29:21-0500, Chang Liu wrote: > > I just added a LICENSE file which is GPLv3. > > Good choice! > > > I'm honestly not sure what the difference between GPLv2 and GPLv3 > > There are modest differences, but the general thrust of both versions of > the license is the same: guaranteed access to source code under a "share > and share alike" principle. > > > is so I went with the latest version (I assume they are compatible?) > > Technically, no. But most GPLv2 software is licensed under terms that > allow promotion of the license to "any later version". One famous > example of an exception that is GPLv2-only is the Linux kernel. > So is seL4 itself[1]. Consider whether you expect to need to share code > with a GPLv2-only project. (Even if you do, I would only revisit your > decision once concrete code-sharing is imminent.) > > You're not stuck with a choice of a single license forever. The GPLv3 > is a good selection to start with (in my opinion) because most > organizations that would like to exploit a work for proprietary > advantage are allergic to that license. > > You can always relicense a work under more permissive terms later if > doing so would align better with your goals. Going from more permissive > terms (like a BSD-style license) to a copyleft (like any version of the > GPL) can be impractical, or result in unintended consequences, because > it is arguably impossible to rescind the permissive license on the older > versions of the code--unless you have an Apple- or Oracle-sized budget > for lawyers to intimidate rivals maintaining the old code base. > > There is probably a better forum for licensing discussions, but my view > is that you've made a perfectly reasonable choice, one that situates > your project squarely and clearly within the Free Software community, > while still leaving you the option to reconsider later. > > Regards, > Branden > > [1] https://microkerneldude.org/2019/12/09/what-does-sel4s-license-imply/ >

1 0

Announcing Neptune OS release v0.1.1: A Windows NT personality for seL4
by Chang Liu 23 Feb '22

23 Feb '22

Hi list, For the past several months I have been working on a project which is to implement a Windows NT personality for the seL4 microkernel, which I have now taken to call “Neptune OS”, named after the codename for Windows 2000. The project has reached the point where I have implemented enough NT primitives such that a keyboard driver stack (taken from the ReactOS source code) can be loaded (as a user process), as well as a command prompt (shell), which is also taken from the ReactOS source code (albeit a very early version of ReactOS). These are all kernel-mode Windows device drivers that I’m running as user processes under seL4. The project is now on github: github.com/cl91/NeptuneOS. The entire system fits in a floppy (download link: github.com/cl91/NeptuneOS/releases/tag/v0.1.0001) Check it out! I think it’s cool! For the next release I’m planning to port the PCI stack, the AHCI stack, and a basic file system (probably fastfat.sys).

4 5

seL4 developer hangout/video call
by Birgit Brecknell 21 Feb '22

21 Feb '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: * Sydney: Wed, Feb 23, 8am * Central Europe: Tue, Feb 22, 10pm * US Pacific Time: Tue, Feb 22, 1pm (There are too many time zones in the world to cite them all :)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au seL4 Foundation, birgit(a)sel4.systems 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Ability to change bench app options for RiscV
by Nataliya Korovkina 12 Feb '22

12 Feb '22

Hi, Does anyone remember why sel4bench configuration for RiscV was not allowed to change bench app options? If it was skipped because it was not necessary then I'd like to fix it. I would add a line to https://github.com/seL4/sel4bench/blob/master/apps/sel4bench/CMakeLists.txt --- a/apps/sel4bench/CMakeLists.txt +++ b/apps/sel4bench/CMakeLists.txt @@ -35,14 +35,15 @@ config_string( # Default dependencies on kernel benchmarking features. Declared here so that # all the benchmark applications can use it if( (KernelArchX86 AND KernelExportPMCUser AND KernelX86DangerousMSR) OR (KernelArchARM AND KernelArmExportPMUUser) OR (KernelArchArmCortexA8 AND KernelDangerousCodeInjection) + OR (KernelArchRiscV) ) set(DefaultBenchDeps TRUE) else() set(DefaultBenchDeps FALSE) endif() find_package(musllibc REQUIRED) Thanks, Nataliya

2 1

How to build compile seL4 along with another C++ project that includes <stdlib.h>
by christinefragoso＠protonmail.com 12 Feb '22

12 Feb '22

I want to run my C++ project in a camkes image for i.mx6. This image should be statically linked. I have a camkes app in https://github.com/seL4/camkes-manifest. The app's CMakeLists.txt includes my project with add_subdirectory("${CMAKE_CURRENT_LIST_DIR}/workspace_DDSHelloWorld"), which is a simple DDS example https://fast-dds.docs.eprosima.com/en/latest/fastdds/getting_started/simple… that also uses CMake as its build system. The entire app is built with ../init-build.sh -DPLATFORM=sabre -DCAMKES_APP=dds. However, the build fails. 1. My project includes <stdint.h>, but sel4 uses the -nostdinc and -nostdinc++ flags, so I get the error "stdint.h: No such file or directory". How do I make my C++ project include seL4's musllibc instead? 2. My project includes other C++ headers like <functional>. Is there any way to build seL4 with C++ headers?

2 1

testing rust program in sel4webserver example project
by lfern70＠gmail.com 12 Feb '22

12 Feb '22

Hi, I am trying to compile a simple rust web server to be executed in the virtual machine (as lighthttpd works in this webserver project). This server works perfect (I am using qemu for testing -aarch64), but when I try to get some random bytes using the rand crate the program hangs: .... let mut key = vec![0u8; 32]; rand::thread_rng().fill_bytes(&mut key); ... Do anybody knows if this could be related to some missing settings (in qemu command line or in some device.camkes file) or some rust features that don't work in a sel4 VM?? Thanks

2 1