August 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

CAmkES Linux VM - Networking
by Cedric MAIRE 27 Aug '20

27 Aug '20

Dear seL4 developers, I am running the CAmkES VM examples from `https://github.com/seL4/camkes-vm-examples` and am able to boot the `minimal` example with: ``` $ ../init-build.sh -DSIMULATION=TRUE -DCAMKES_VM_APP=minimal $ ninja $ qemu-system-x86_64 -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-image-ia32-pc99 --enable-kvm -smp 2 -cpu Nehalem,+vmx -nographic ``` However this example does not provide networking capabilities due to missing drivers (is that correct?). Is there a simple way I may add networking? Simply put I would like the Linux guest to be able to connect to the internet. I tried passing the QEMU parameters to setup a tap interface, which didn't help. I also tried to use the example `cma34cr_centos` which should already provide networking but when I try to boot this example using `qemu-system-x86_64 -m 2048 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 --enable-kvm -smp 2 -cpu Nehalem,+vmx -nographic` I get the following error: `create_objects@main.c:794 Ran out of untyped memory while creating objects.`. Full log output in the `.log` file. Thanks in advance, Best regards, Cedric Maire =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. ===============================================================================

1 0

some question about sched_ctrl of mcs答复: some question about mcs
by yadong.li 26 Aug '20

26 Aug '20

Hi Kent： Firstly，thank you for your information. I found the test code call "simple_get_sched_ctrl(&env->simple, 0)" function to get sched_ctrl cap, but I feel confused about env->simple. I have two question about sched_ctrl when I want to add mcs call function for camkes-arm-vm project Background: I try to add get sched_ctrl cap before seL4_TCB_Configure of vm_create_vcpu_arch(projects/seL4_projects_libs/libsel4vm/src/arch/arm/boot.c) 1. I try use "simple_get_sched_ctrl(vm->simple, affinity);" or " simple_default_init_bootinfo(&simple, platsupport_get_bootinfo()) simple_get_sched_ctrl(simple, affinity);" But they all failed What "simple" should I used to get sched_ctl in this project. 2. I found camkes_simple_sched_ctrl in component.simple.c generate C code, have below code: /*- if 'sched_ctrl' in configuration[me.name].keys() -*/ But I did not found camkes configurations have "sched_ctrl" field in project or your examples in CAmkES Thank you very much -----邮件原件----- 发件人: Kent Mcleod [mailto:kent.mcleod72@gmail.com] 发送时间: 2020年8月25日 10:37 收件人: yadong.li 抄送: devel(a)sel4.systems 主题: Re: [seL4] some question about mcs > > Hi, > 1.Did seL4-11.0.0<https://docs.sel4.systems/releases/sel4/11.0.0> support mcs, I found some CONFIG_KERNEL_MCS in this release version ? or must use seL4 10.1.1-mcs <https://docs.sel4.systems/releases/sel4/10.1.1-mcs.html> branch? > 2'Where I can find some example about mcs in project? The introduction of Wiki is too simple , I can 't make the param of seL4_SchedControl_Configure is correct? > > Thank you very much 11.0.0 does introduce a config option CONFIG_KERNEL_MCS (KernelIsMCS in CMake). You could start with the MCS tutorial: https://docs.sel4.systems/Tutorials/mcs.html. Alternatively, there are MCS tests in seL4test: https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/… or examples in CAmkES: - https://github.com/seL4/camkes/tree/master/apps/cms-donate - https://github.com/seL4/camkes/tree/master/apps/cs-donate - https://github.com/seL4/camkes/tree/master/apps/cs-nodonate - https://github.com/seL4/camkes/tree/master/apps/periodic - https://github.com/seL4/camkes/tree/master/apps/event-driven - https://github.com/seL4/camkes/tree/master/apps/mcs-donate - https://github.com/seL4/camkes/tree/master/apps/mcs-nodonate I'm not aware if there is any documentation about the CAmkES app examples, but I believe they are supposed to demonstrate different scheduling scenarios using MCS. > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel

1 0

"Ran out of untyped memory"
by Michael Neises 25 Aug '20

25 Aug '20

Hello, I'm trying to build a camkes app, but when I attempt to run it on an Odroid-xu4, I get the following error just before the boot halts: "Ran out of untyped memory while creating objects" I've narrowed the error down to two calls to a this function: https://github.com/SEL4PROJ/camkes-vm-linux/blob/dc354df3222766b9d366725751… When I use only one call, the image boots nicely. If I use both calls, I get the above error. My understanding is that this function simply adds an executable to the filesystem, so I'm not sure how to begin debugging this. Is it possible that the filesystem is actually "too big" for sel4 to boot successfully? Please advise! Best, Michael Neises

3 4

some question about mcs
by yadong.li 25 Aug '20

25 Aug '20

Hi, 1.Did seL4-11.0.0<https://docs.sel4.systems/releases/sel4/11.0.0> support mcs, I found some CONFIG_KERNEL_MCS in this release version ? or must use seL4 10.1.1-mcs <https://docs.sel4.systems/releases/sel4/10.1.1-mcs.html> branch? 2'Where I can find some example about mcs in project? The introduction of Wiki is too simple , I can 't make the param of seL4_SchedControl_Configure is correct? Thank you very much

2 1

Trouble getting a custom kernel to boot under sel4 on a tk1 board
by Travis Wheatley 24 Aug '20

24 Aug '20

I am having difficulty getting a custom kernel to boot under sel4 on a tk1 board. I have no problems building and booting an image that uses the pre-built linux-tk1-initrd file found in the projects/vm/linux folder. Howoever, when I build a “custom” kernel using buildroot-2016.08.1 as specified in this<https://docs.sel4.systems/projects/camkes-arm-vm/> the boot process hangs shortly after it loads the dtb. <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffc2d400 "rootserver" @106f0]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> Loading Linux: 'linux' dtb: 'linux-dtb' install_linux_devices(a)main.c<mailto:install_linux_devices@main.c>:605 module name: map_frame_hack install_linux_devices(a)main.c<mailto:install_linux_devices@main.c>:605 module name: plat I am using the buildroot_tk1_initrd_defconfig file, also located in the projects/vm/linux folder. I am simply replacing the linux-tk1-initrd file in projects/vm/linux with the image file that gets created in the buildroot-2016.08.1/output/build/linux-custom/arch/arm/boot folder. I then clean my build directory and do the requisite “../init-build.sh -DPLATFORM=tk1 -DCAMKES_VM_APP=vm_minimal” followed by “ninja”. I then put the capdl-loader-image-arm-tk1 file on an SD card, put it in the Tk1 and do: “fatload mmc 1 0x82000000 <filename>” followed by “bootefi 0x82000000” Assuming the guidance on buildroot and the defconfig supplied match what was used to create the working pre-built linux-tk1-initrd kernel the “custom” kernel I built should be very similar. So, what am I missing? Why would a custom kernel hang at the above mentioned point in the boot process?

1 0

Porting Sel4 with RPi 3B+
by 萧琒 20 Aug '20

20 Aug '20

Hi, Professional Devel Support of Sel4, We are porting Sel4 with RPi 3B+, but we fail to boot RPi 3B+ with Sel4 successfully. We cann't find the problem, please help us. we follow the Steps: 1. Use Raspberry Pi Imager v1.4 to burn the operation system (Raspberry Pi OS Lite 32bit) on SD card, and it works well with hardware of RPi 3B+. 2. Build Sel4test-manifest: 2.1 clone the repo of https://github.com/seL4/sel4test-manifest.git 2.2 build image with ../init-build.sh -DPLATFORM=rpi3 -DAARCH32=1 2.3 the image file (sel4test-driver-image-arm-bcm2837) is produced successfully. 3. Following the SD card setup, Copy the following files to root direcctory of SD. 3.1 sel4test-driver-image-arm-bcm2837 3.2 bootcode.bin and start.elf from https://github.com/raspberrypi/firmware/tree/master/boot 3.3 u-boot.bin downloaded from https://sel4.systems/Info/Docs/u-boot-working-rpi3-32bit-v2017.11.bin 3.4 Add enable_uart=1 and kernel=u-boot.bin to the bottom of config.txt 3.5 uboot.env, we fail to find the file, so we don't use the file. if you know the step to produce uboot.env, please lead us. 4. Re-insert SD into the RPi3B+, and power the RPi3B+ on, the RPi3B+ shows the U-Boot successfully. 4.1 sel4test-driver-image-arm-bcm2837 image file’s name printed out with the command of "fatls mmc 0" 4.2 fatload the image with command of "fatload mmc 0 0x10000000 sel4test-driver-image-arm-bcm2837", the result: reading sel4test-driver-image-arm-bcm2837 4791000 bytes read in 406 ms (11.3 MiB/s) 4.3 bootelf 0x10000000, the result: CACHE: Misaligned operation at range [0082a000, 0082a034] CACHE: Misaligned operation at range [0082b000, 00834fcc] CACHE: Misaligned operation at range [00834fcc, 00835b07] CACHE: Misaligned operation at range [00c9be40, 00c9be9c] CACHE: Misaligned operation at range [00c9be9c, 00c9bec8] ## Starting application at 0x0082a000 ... Then, RPi3B+ is blocked and without anything else to display ! ---- Thanks, Alen 肖月振（萧琒）阿里云事业群-IOT事业部-飞天六十四部电话：13391191786 邮箱：yuezhen.xyz(a)alibaba-inc.com

2 1

Re: [seL4] Devel Digest, Vol 75, Issue 8
by Cedric MAIRE 19 Aug '20

19 Aug '20

Hi Luke, Thanks for your help! I just tried out your solution and get back the following error: `groupmod: GID '1000' already exists`. Here is the workflow that I follow: ``` $ git clone https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git $ cd ~/sel4/seL4-CAmkES-L4v-dockerfiles/ $ git pull # Make sure to be up-to-date. $ git checkout fix_rust $ git pull # Make sure to be up-to-date. `fix_rust` is ahead of `master` so no missing commits. $ ./build.sh -p -b camkes -s rust $ make user CAMKES_IMG=camkes-rust HOST_DIR="~/sel4/" ``` I attached a more detailed log of the error I get. The command throwing this is (full command in log file): `/bin/sh -c groupadd -fg ${GID} ${GROUP} [...] && chmod -R ug+rw /home/${UNAME}` Does this look familiar to you? Best, Cedric -----Original Message----- From: Devel <devel-bounces(a)sel4.systems> On Behalf Of devel-request(a)sel4.systems Sent: samedi, 15 août 2020 04:00 To: devel(a)sel4.systems Subject: Devel Digest, Vol 75, Issue 8 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel?mc_phishing_protection_id=28047-b… or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Dockerfiles - "camkes-rust" Image (Mondy, Luke (Data61, Kensington NSW)) ---------------------------------------------------------------------- Message: 1 Date: Fri, 14 Aug 2020 06:29:32 +0000 From: "Mondy, Luke (Data61, Kensington NSW)" <Luke.Mondy(a)data61.csiro.au> To: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] Dockerfiles - "camkes-rust" Image Message-ID: <SYAPR01MB25284E1D39674828FDC11EBED5400(a)SYAPR01MB2528.ausprd01.prod.outlook.com> Content-Type: text/plain; charset="us-ascii" Hello Cedric, Thanks for the report. I believe the best way to use the camkes-rust image is to run this: make user CAMKES_IMG=camkes-rust However, in saying that, it unfortunately does not perform quite as hoped. Because of the way the code is built, it ends up putting the Cargo/Rust content into /root/.cargo, which is inaccessible to you as a non-root user. This is an oversight on my part, as unfortunately these interactive bits of the Dockerfile system don't get tested automatically. I've made a PR on GitHub, which shows the fixes needed: https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles/pull/24 Note that the master branch has also been recently updated, so you may need to pick further commits from there (or simply pull them all down first) for things to work. Let me know if that helps. Cheers, Luke -- Dr Luke Mondy, Systems Administrator, P +61 2 9490 5773 | https://ts.data61.csiro.au/?mc_phishing_protection_id=28047-bsrk3aadu815grd… Trustworthy Systems | DATA61 | CSIRO CSIRO Staff Association Delegate Hours at CSIRO Monday: 9:00am to 5pm Tues, Wed, Fri: 1:30pm to 5pm ________________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of Cedric MAIRE <cmaire(a)icrc.org> Sent: Friday, 14 August 2020 2:42 AM To: devel(a)sel4.systems Subject: [seL4] Dockerfiles - "camkes-rust" Image Dear seL4 developers, I am using the provided dockerfiles repository to build the docker images in order to compile seL4. I would like to add a rust compiler to my docker image, which I do with "./build.sh -p -b camkes -s rust". This builds an image tagged "trustworthysystems/camkes-rust". I would like to launch this image in a container using the "Makefile" as I would do for the "trustworthysystems/camkes" image (using "make user"). I tried adding targets to the "Makefile" file changing the "USER_BASE_IMG" variable to use "trustworthysystems/camkes-rust" instead of "trustworthysystems/camkes", without success. I also tried to force the image by renaming/retagging "trustworthysystems/camkes " to "trustworthysystems/camkes-old" and "trustworthysystems/camkes-rust" to "trustworthysystems/camkes ". I also forced every base image to be the one containing the Rust compiler (in "Makefile"). All without success. For some reason "trustworthysystems/camkes-rust" image is never used. If I start it manually using docker commands I am able to launch and attach to it, getting the expected Rust compiler. Through the "Makefile" it ever only uses "trustworthysystems/camkes" without the Rust compiler. Is there an easy way to get this to work? What am I missing? Best regards, Cedric =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. =============================================================================== _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel?mc_phishing_protection_id=28047-b… ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel?mc_phishing_protection_id=28047-b… ------------------------------ End of Devel Digest, Vol 75, Issue 8 ************************************ =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. ===============================================================================

2 1