January 2020 - Devel - lists.sel4.systems

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

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

Problem booting camkes arm vmm on TK1 from SD Card
by Mike Clark 10 Feb '20

10 Feb '20

I'm using the docker image to build the CAmkES ARM VMM project using roughly the instructions here: https://docs.sel4.systems/VM/CAmkESARMVM.html (they are slightly out of date). I do: ../init-build.sh -DAARCH32=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tk1 ninja Then I copy the resulting image from the images directory to an SD card and put that in my TK1. When U-Boot starts I use the following commands to try to boot fatload mmc 1 0x10000000 capdl-loader-image-arm-tk1 bootelf 0x10000000 To which I get an error: No elf image at address 0x10000000 I tried with an older version of U-Boot (that worked following this same procedure about a year ago). It is U-Boot SPL 2014.10-rc2-g3127911 (Jun 07 2016 - 21:00:01) I also tried updating U-Boot to U-Boot SPL 2020.01-00442-gc00bd81ae0 (Jan 10 2020 - 11:10:18 -0500). Same error. Any thoughts or suggestions on how I get this to boot?

4 14

GPIO on Sabre imx6
by Parvaneh Ahgajani 09 Feb '20

09 Feb '20

Hello all, I am working with sabre lite board and using camkes framework. In my implementation I have a driver component that has 7 dataport buf and I connected these buffers to hardware component. In source of component driver I am initialize gpio_sys, mux_sys and pins using these functions: - imx6_mux_init() - imx6_gpio_sys_init() - gpio_new() Here I have copied some part of my code: ****************************************** gpio_sys_t gpio_sys; gpio_t pins[32*7]; mux_sys_t mux_sys; void gpio__init() { imx6_mux_init(NULL, &mux_sys); imx6_gpio_sys_init((void*)gpio0, (void*)gpio1, (void*)gpio2, (void*)gpio3, (void*)gpio4, (void*)gpio5, (void*)gpio6, &mux_sys, &gpio_sys); } void gpio_init_pin(int pin, int direction) { if(pin>0 && pin< sizeof(pins)/sizeof(pins[0])) { gpio_new(&gpio_sys, pin, (enum gpio_dir)direction, &pins[pin]); } } void gpio_set_pin(int pin, int value) { if(pin >= 0 && pin < (sizeof(pins)/sizeof(pins[0]))) { if(value) { gpio_set(&pins[pin]); } else { gpio_clr(&pins[pin]); } } } int gpio_read_pin(int pin) { if(pin>0 && pin< sizeof(pins)/sizeof(pins[0])) { return gpio_get(&pins[pin]); } return -1; } ****************************************** By calling "gpio_init_pin(ALARM_PIN= 28, 0);" I am getting this error: Assertion failed: bank->data == v (PATH/projects/util_libs/libplatsupport/src/plat/imx6/gpio.c: imx6_gpio_write: 144) How can I fix this error? How should I specify the GPIO pins? Thank you for your time and consideration, Parvaneh.

2 3

Configuring CAmkES projects
by Grant Jurgensen 01 Feb '20

01 Feb '20

Hi everyone, I have a couple questions regarding the current CMake build structure for CAmkES projects. It seems that the current structure intends you to put your project in the camkes/apps folder, and then build your project with `../init-build -DCAMKES_APP=<project_name>`, or the equivalent using the griddle script. What I don't understand is how you are supposed to configure your project. It seems easy_settings.cmake is always loaded. Is it advisable to edit this file? In the past, I could also tweak configuration variables manually by invoking the ccmake gui on the top-level directory. Now that there is no CMakeLists.txt in the top-level directory, this does not work. If I try it in my project's directory, it tells me the cache is empty. Is it still possible to edit CMake cache variables with ccmake? Thanks! Grant Jurgensen

2 2

Recycle resources used by a thread after it terminates
by Alexandre Mutel 01 Feb '20

01 Feb '20

Hi, I have a design question regarding how to recycle capabilities/memory frames that were used by a thread once it terminates. Let's assume that there is a MemoryManager server responsible to serve virtual memory to user processes (e.g similar to implementing VirtualAlloc). The MemoryManager has to maintain the list of untyped object, retype them, maintain likely a list of resources allocated for a user thread, likely copy/mint the page frames to forward them to the user process...etc. But when a thread terminates, as I can't see any related events in seL4, I would assume that the user process would have to explicitly notify the MemoryManager on exit. Then the MemoryManager would know which user thread has exited and would update/recover the used capabilities and destroy them, in order to recover untyped objects. Would it be a proper design that plays well with seL4? Do you think that it could be done more efficiently with seL4? Thank you!

2 2

AMD CPUs and SMP scalability
by Demi M. Obenour 30 Jan '20

30 Jan '20

My understanding is that seL4 plans on scaling to large multi-core server processors by using Intel TSX. However, AMD has not implemented TSX, and TSX has been involved in many recent side-channel attacks. AMD systems are attractive both from a performance and a security perspective, but my understanding is that the performance of seL4 on them will be terrible. Are there plans to implement and verify a version of seL4 that scales to multicore AMD server-class CPUs? The problem with a multikernel is that not having thread migration is likely to cause starvation on many practical workloads Sincerely, Demi

2 2

Status of side-channel attack mitigation
by Demi M. Obenour 30 Jan '20

30 Jan '20

What is the current status of seL4 with respect to Meltdown, Spectre, L1TF, MDS and other CPU vulnerabilities? Thank you, Demi

2 2

(no subject)
by abdi mahmud haji 29 Jan '20

29 Jan '20

hi i have been wondering how can i install or put another OS( like , window ,linux )on the top of seL4 microkernel can some one help

2 1