March 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

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

Build failure for sel4 on raspberry pi 5
by l4＠photiczone.com 14 Aug '24

14 Aug '24

Hi everyone, I am getting a link failure during the build of sel4test-tests: /usr/bin/ld: apps/sel4test-driver/musllibc/build-temp/stage/lib/libc.a(__stdio_exit.o): copy relocation against non-copyable protected symbol `__stdin_used' collect2: error: ld returned 1 exit status Searching t'interwebs seems to imply this is a gnarly problem caused by the nuances of various build tools - but one that should not apply to Arm. You can summarise everything I did before the build like this: sudo apt install ninja-build libxml2-utils repo pip3 install pyyaml typing hardware pyfdt jinja2 jsonschema six future ply python3-protobuf grpcio-tools cd && mkdir xxx && cd xxx Then to follow your build repo init -u https://github.com/seL4/sel4test-manifest.git repo sync mkdir build && cd build ../init-build.sh -DPLATFORM=bcm2711 ninja And yes I know it is not supported and the BCM2711 is for the Pi 4. I am evaluating ;) Any help greatly appreciated. Thanks, Smiley

3 4

question about the seL4/camkes-vm-examples
by PX 15 Apr '24

15 Apr '24

Hi,All I am trying to build the seL4 VMM example for the qemu-arm-virt platform from seL4/camkes-vm-exmaples. I can build the vmm image successfully, but I cannot run the image. Here are what I did: 1. I use the "../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt" command. 2. ninja After these two steps, the vmm image, capdl-loader-image-arm-qemu-arm-virt is successfully built. But when I run the generated scripts, ./simulate, to run the VMM on qemu, the vmm fails to boot up. The error message is attached below. I use Ubuntu 20.04 and QEMU emulator version 4.2.1. Do I miss something here? Do I use the correct version of the building environment? Any help would be appreciated! ./simulate ./simulate: QEMU command: qemu-system-arm -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a15 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p1 paddr=[61805000..62c02ebf] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 6192264c. Loaded DTB from 6192264c. paddr=[60042000..60043fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60041fff] vaddr=[e0000000..e0041fff] virt_entry=e0000000 ELF-loading image 'capdl-loader' to 60044000 paddr=[60044000..6140cfff] vaddr=[10000..13d8fff] virt_entry=1880c Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. available phys memory regions: 1 [60000000..c0000000] reserved virt address space regions: 4 [e0000000..e0042000] [e0042000..e0043da9] [e0044000..e140d000] [ff000000..ff200000] Booting all finished, dropped to user space *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 65536 bytes needed, 0 bytes available).>>* run@main.c:1332 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1) install_vm_devices@main.c:704 module name: map_frame_hack install_vm_devices@main.c:704 module name: init_ram Loading Kernel: 'linux' Loading Initrd: 'linux-initrd' Loading Generated DTB -------- *Pagefault from [vm0]: read prefetch fault @ PC: 0x4 IPA: 0x4, FSR: 0x6* *Context:* *r0: 0x0* *r1: 0xffffffff* *r2: 0x4f000000* *r3: 0x0* *r4: 0x0* *r5: 0x0* *r6: 0x0* *r7: 0x0* *r8: 0x0* *r9: 0x0* *r10: 0x0* *r11: 0x0* *r12: 0x0* *pc: 0x4* *r14: 0x0* *sp: 0x0* *cpsr: 0x9b* m-------- main_continued@main.c:1310 Failed to run VM Halting...

3 4

sel4test CACHEFLUSH0001 failed
by Leonid Meyerovich 29 Mar '24

29 Mar '24

Hello, I run sel4test on the aarch64 platform. My CACHEFLUSH0001 test in sel4test failed /* Clean makes data observable to non-cached page */ *ptr = 0xC0FFEE; *ptrc = 0xDEADBEEF; test_assert(*ptr == 0xC0FFEE); test_assert(*ptrc == 0xDEADBEEF); I have tried to make to 'improve' memory/cache coherence, but the last assertion still failed /* Clean makes data observable to non-cached page */ *ptr = 0xC0FFEE; *ptrc = 0xDEADBEEF; error = seL4_ARM_Page_Clean_Data(framec, 0, PAGE_SIZE_4K); error = seL4_ARM_Page_Invalidate_Data(framec, 0, PAGE_SIZE_4K); __asm volatile("dmb sy" ::: "memory"); test_assert(*ptr == 0xC0FFEE); test_assert(*ptrc == 0xDEADBEEF); Thank you, Leonid

2 2

Re: Only 512mb ram available on capdl-loader-image-arm-qemu-arm-virt image
by Peter Chubb 26 Mar '24

26 Mar '24

>>>>> "Daniele" == Daniele Feliciani <felicianidaniele(a)gmail.com> writes: Daniele> Hello Peter, I have the same Daniele> problem. i tried to change the guest ram value to Daniele> 0x40000000. I added set(QEMU_MEMORY "2048") in config.cmake Daniele> but I get the following errors while running : " Daniele> map_vm_memory_reservation@guest_memory.c:477 Failed to get Daniele> frame for reservation address 0x60000000" and " Daniele> vm_ram_touch@guest_ram.c:165 Failed to touch ram region: Not Daniele> registered RAM region 32 bit ARM insts not decoded" Check the size of the MMIO region. By default it uses 29 bits; for a 2G region you need 31 bits. In the devices.camkes file, in the untyped_mmios section. There's probably an entry, "0x40000000:29", try increasing this to "0x40000000:31" to get a 2^31 region. -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

3 3

Re: Only 512mb ram available on capdl-loader-image-arm-qemu-arm-virt image
by Daniele Feliciani 25 Mar '24

25 Mar '24

It doesn't seem to work. I'm attaching the device.camkes file and the error screenshots. Il giorno lun 25 mar 2024 alle ore 10:43 Peter Chubb < peter.chubb(a)unsw.edu.au> ha scritto: > >>>>> "Daniele" == Daniele Feliciani <felicianidaniele(a)gmail.com> writes: > > Daniele> I changed the value but now i > Daniele> have the following error: > > Danielle> ./simulate: QEMU command: qemu-system-aarch64 -machine > Danielle> virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 > -nographic > Danielle> -m size=2048 -kernel > images/capdl-loader-image-arm-qemu-arm-virt > Danielle> ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 > Danielle> paddr=[61b07000..62ee00b7] > Danielle> No DTB passed in from boot loader. > Danielle> Looking for DTB in CPIO archive...found at 61c07c68. > Danielle> Loaded DTB from 61c07c68. > Danielle> paddr=[60242000..60243fff] > Danielle> ELF-loading image 'kernel' to 60000000 > Danielle> paddr=[60000000..60241fff] > Danielle> vaddr=[8060000000..8060241fff] > Danielle> virt_entry=8060000000 > Danielle> ELF-loading image 'capdl-loader' to 60244000 > Danielle> paddr=[60244000..6170cfff] > Danielle> vaddr=[400000..18c8fff] > Danielle> virt_entry=408d88 > Danielle> Enabling hypervisor MMU and paging > Danielle> Jumping to kernel-image entry point... > Danielle> > Danielle> Bootstrapping kernel > Danielle> Warning: Could not infer GIC interrupt target ID, assuming 0. > Danielle> available phys memory regions: 1 > Danielle> [60000000..c0000000] > ^^^^^^^^^ this is the physical memory region you have to play > with. Make the region given to the VM start at 0x60000000 > instead of 040000000 > > -- > Dr Peter Chubb https://trustworthy.systems/ > Trustworthy Systems Group CSE, UNSW > Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm. >

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 25 Mar '24

25 Mar '24

Hi all A friendly reminder that the seL4 developer hangout is on next week: * Wed Apr 3, 7am UTC For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Only 512mb ram available on capdl-loader-image-arm-qemu-arm-virt image
by skydivebcn＠gmail.com 25 Mar '24

25 Mar '24

Hi! I'm running a an aarch64 Linux guest with qemu with "qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -m size=2048 (...) -kernel capdl-loader-image-arm-qemu-arm-virt". I have noticed that no matter how I set the "-m size" parameter that only 512MB are available to the Linux guest. Removing the "highmem=off" crashes the system. Ok, what is the fastest, easiest way to get a workaround to this (if possible)? and have much more RAM available to Linux guest? Best,

2 1

next seL4 TSC meeting on Fri 22 Mar
by Gerwin Klein 20 Mar '24

20 Mar '24

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Fri, 22 Mar, 6pm - Central Europe: Fri, 22 Mar, 8am - US West Coast (LA/SF): Fri, 22 Mar, 0:00h See also the seL4 calendar feed available from here: https://sel4.systems/contact/home.pml The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/83417411537 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - action items from last meeting - RFC-17: IPI API - RFC-16: PMU (for discussion/feedback, not enough detail yet to vote) - RFC-15: Morello (for discussion/feedback, not enough detail yet to vote) - RFC-14: MCS budget limit thresholds — status? - should we remove deprecated sel4lib functions to enable verification? - steps for next seL4 release - discussion if there is time: - use GitHub discussions instead of discourse? (i.e. retire discourse?) - use GitHub for RFC process? (i.e. retire/archive JIRA?) If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems

1 0