June 2021 - 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

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

ethernet pass-through using CAmkES VM on x86
by meshkat os 29 Sep '21

29 Sep '21

hi I am new to camkes VM on x86. I want to connect the guest to the host via the ethernet network. and I used this ( https://docs.sel4.systems/projects/camkes-vm/) tutorial to create pass-through in minimal example x86. run in qemu on ubuntu 17.10. but the guest os doesn't create an ethernet interface. I also tested zmq example this is qemu options: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-image-ia32-pc99 and minimal.camkes configs: configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0) vm0.simple_untyped23_pool = 20; vm0.heap_size = 0x2000000; vm0.guest_ram_mb = 128; vm0.kernel_cmdline = VM_GUEST_CMDLINE; vm0.kernel_image = "bzimage"; vm0.kernel_relocs = "bzimage"; vm0.initrd_image = "rootfs.cpio"; vm0.iospace_domain = 0x0f; vm0_config.pci_devices_iospace = 1; vm0_config.ioports = [ {"start":0x4080, "end":0x4090, "pci_device":0x1f, "name":"SATA"}, {"start":0x4090, "end":0x40a0, "pci_device":0x1f, "name":"SATA"}, {"start":0x40b0, "end":0x40b8, "pci_device":0x1f, "name":"SATA"}, {"start":0x40b8, "end":0x40c0, "pci_device":0x1f, "name":"SATA"}, {"start":0x40c8, "end":0x40cc, "pci_device":0x1f, "name":"SATA"}, {"start":0x40cc, "end":0x40d0, "pci_device":0x1f, "name":"SATA"}, {"start":0x3000, "end":0x3020, "pci_device":0, "name":"Ethernet5"}, ]; vm0_config.pci_devices = [ { "name":"SATA", "bus":0, "dev":0x1f, "fun":2, "irq":"SATA", "memory":[], }, { "name":"Ethernet5", "bus":5, "dev":0, "fun":0, "irq":"Ethernet5", "memory":[ {"paddr":0xc0500000, "size":0x20000, "page_bits":12}, {"paddr":0xc0520000, "size":0x4000, "page_bits":12}, ], }, ]; vm0_config.irqs = [ {"name":"SATA", "source":19, "level_trig":1, "active_low":1, "dest":11}, {"name":"Ethernet5", "source":0x11, "level_trig":1, "active_low":1, "dest":10}, ]; } thanks

4 4

gic v2 vs gic v3
by Chris Koziarz 09 Jul '21

09 Jul '21

Hi all, I'm trying to port camkes-arm-vm to a different platform, that supports gic-v3 In the process, I hit a compilation error: Building C object kernel/CMakeFiles/kernel_all_pp_...rapper_temp_lib.dir/ kernel_all_pp_prune_wrapper_temp.c.obj FAILED: kernel/kernel_all_pp_prune_wrapper_temp.c In file included from /home/chris/camkes-tqma8xqp- vm/kernel/src/arch/arm/object/vcpu.c:15: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v2.h:23: error: "IRQ_MASK" redefined [-Werror] 23 #define IRQ_MASK MASK(10u) In file included from kernel/gen_headers/plat/platform_gen.h:23, from /home/chris/camkes-tqma8xqp-vm/kernel/include/plat/ default/plat/machine.h:8, from /home/chris/camkes-tqma8xqp- vm/kernel/include/machine.h:9, from /home/chris/camkes-tqma8xqp- vm/kernel/include/api/syscall.h:10, from /home/chris/camkes-tqma8xqp- vm/kernel/src/api/faults.c:10: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v3.h:30: note: this is the location of the previous definition 30 #define IRQ_MASK MASK(16u) which is an indicative that both gic_v3.h & gic_v2.h headers have been included, which is an error because said headers are not compatible: kernel/include/arch/arm/arch/machine/gic_v3.h:#define IRQ_MASK MASK(16u) kernel/include/arch/arm/arch/machine/gic_v2.h:#define IRQ_MASK MASK(10u) So my question is: how can I configure the build to avoid such a conflict? I can grepp the relevant configuration option in CMakeCache.txt: build_tqma8/CMakeCache.txt:CONFIGURE_INTERRUPT_CONTROLLER:INTERNAL=arch/machine/gic_v3.h but cannot see it in ccmake gui because it's "INTERNAL" What is the solution? - replace this option somehow to use gic_v2 and have my HW use gic v.2, or - change compilation options to use gic_v3 everywhere Thanks for any help, Chris.

4 5

Re: Tutorial Problem
by Kent Mcleod 08 Jul '21

08 Jul '21

On Wed, Jun 30, 2021 at 11:53 AM Michael Neises <neisesmichael(a)gmail.com> wrote: > > Kent, > > > > I tried using those extra arguments and got the same error regarding kvm I reported a few minutes ago: > > > > ./simulate: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,+syscall,+lm,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 Could not access KVM kernel module: No such file or directory > > qemu-system-x86_64: failed to initialize KVM: No such file or directory > There are instructions on how to setup KVM and nested virtualization on the tutorial that I've pasted here: "Note if you are using QEMU it is important to ensure that your host machine has VT-x support and KVM (https://www.linux-kvm.org/page/Main_Page) installed. You also need to ensure you have enabled nested virtulisation with KVM guests as described here (https://www.linux-kvm.org/page/Nested_Guests)" A quick way to check if nested virtualization is enabled (and therefore supported) on your host is to run `cat /sys/module/kvm_intel/parameters/nested`. `Y` should be returned if it's enabled. It may be easier to run the image on an actual machine instead of in qemu. The images produced can be loaded by a multiboot loader such as grub or pxelinux. (https://docs.sel4.systems/Hardware/VMware/#add-grub2-option-to-run-sel4) has an example grub config.

4 7

seL4 Linux guest mmap() crashes the VM
by Hugo V.C. 02 Jul '21

02 Jul '21

Hi, my seL4 Linux VM box just crashed when trying to access a memory address. Basically I simply wanted to use "devmem" tool to just print the content of a specific address in memory and looked like seL4 was unable to handle the guest OS mmap() correctly. Below the console log: # ls /proc/283/maps /proc/283/maps # cat /proc/283/maps 00400000-00532000 r-xp 00000000 00:02 6023 /bin/lighttpd 00541000-00543000 r--p 00131000 00:02 6023 /bin/lighttpd 00543000-00546000 rw-p 00133000 00:02 6023 /bin/lighttpd 00546000-0054d000 rw-p 00000000 00:00 0 0bd0b000-0bd2d000 rw-p 00000000 00:00 0 [heap] 0bd2d000-0bd91000 rw-p 00000000 00:00 0 [heap] ffff82084000-ffff82085000 r--p 00000000 00:00 0 [vvar] ffff82085000-ffff82086000 r-xp 00000000 00:00 0 [vdso] ffffe6c58000-ffffe6c79000 rw-p 00000000 00:00 0 [stack] # devmem 0xffffe6c58000 8 _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0xffffe6c58000 map_page@mapping.c:68 Failed to map page at address 0xffffe6c58000 with cap 396187, error: 1 sel4utils_map_page_pd@vspace.c:153 Error mapping pages, bailing: 1 map_vm_memory_reservation@guest_memory.c:477 Failed to map address 0xe6c58000 into guest vm vspace vm_map_reservation@guest_memory.c:510 Failed to map vm reservation: Error when mapping into VM's vspace -------- Pagefault from [Linux]: read fault @ PC: 0x414c38 IPA: 0xffffe6c58000, FSR: 0x93020004 Context: x0: 0xffff9cfe6000 x1: 0x0 x2: 0x0 x3: 0x1 x4: 0x3 x5: 0xffffe6c58000 x6: 0x5 x7: 0x20 x8: 0xde x9: 0xffffe539cf54 x10: 0xffff9cfe8050 x11: 0x1 x12: 0x436 pc: 0x414c38 x14: 0xffffffff sp: 0xffffe539bb70 spsr: 0x60000000 x13: 0x1 x15: 0x3 x16: 0xffff9cf486c8 x17: 0x4c3870 x18: 0x0 x19: 0x8 x20: 0x0 x21: 0x4c3000 x22: 0xffffe539bd98 x23: 0xffffe6c58000 x24: 0x0 x25: 0x0 x26: 0x0 x27: 0x0 x28: 0x0 x29: 0xffffe539bc60 x30: 0x414bac m-------- main_continued@main.c:1134 Failed to run VM Halting... My three concerns here are: 1) Why this guest mmap() is crashing the VM? Memory address is valid (just guest user space process stack). 2) Is it possible to have some kind of "dump and reboot VM" when a VM and/or guest OS crashes? 3) Are there any plans to formally verify the seL4's VM camkes code? Thank you!

2 6

Camkes SerialServer and util_libs/libplatsupport with ODROID-C4
by Robert Reid 01 Jul '21

01 Jul '21

Hi everyone Summary - trying to get util_libs/libplatsupport going for a HardKernel ODROID-C4, using the camkes serialserver_polling app - but not having any luck with mapping the UART. I'd welcome any explanations of what you think is happening here. The background and my progress follows. I thought I'd dive into the seL4 world and do some experimenting. I thought a good place to start would be the UNSW AOS project (17 years after I first did it) - but with no more ODROID-C2, got a hold of an ODROID-C4 and figured that would be a good project in itself (and well timed with a Sydney lockdown). So - good news: The peripheral devices we need are all very similar to a C2, so by getting a new DTS file and updating a few addresses it starts off fairly happily. sel4-test builds and runs (All is well...); so does the camkes adder app; and with some mods to provide enough slots (maybe because it has 4GB rather than 2GB) I have got the AOS milestone 0 stub to run (including the uart initialisation). (More work to actually finish m0 and keep going, but a job for later) But then: I moved onto the util_libs / libplatsupport project to try and port over as much of the device settings as possible; and using the camkes app serialserver_polling, under the hood using SerialServer, I can't get the uart to initialiise (or more strictly can't get the uart address to map). chardev_map / ps_io_map fails, returning a vaddr of 0. I've added a bunch of debug prints to the process; and for comparison also run it on QEMU emulating a Sabre board. On odroidc4 hardware: ## Starting application at 0x01080000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A55 r1p0 paddr=[95e000..d5710f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at a86de8. Loaded DTB from a86de8. paddr=[23f000..24afff] ELF-loading image 'kernel' to 0 paddr=[0..23efff] vaddr=[ffffff8000000000..ffffff800023efff] virt_entry=ffffff8000000000 ELF-loading image 'capdl-loader' to 24b000 paddr=[24b000..563fff] vaddr=[400000..718fff] virt_entry=408e48 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space pre_init@serial.c:501 About to init port, io_ops=0x487cf0 ps_cdev_init@chardev.c:46 About to init_fn 3 ps_cdev_init@chardev.c:47 dev_defn[3].paddr: 0xff803000, size 1000 uart_init@serial.c:51 about to chardev_map: dev=0x473948, defn->id=3, defn->padd r=0xff803000 chardev_map@chardev.h:26 ops->io_mapper=0x487be0 &(ops->io_mapper)=0x442728 dev- >paddr=0xff803000 dev->size=0x1000 uart_init@serial.c:56 chardev_map mapped page_vaddr 0 plat_pre_init@plat.c:64 Failed to initialise character device plat_pre_init@plat.c:65 PS_SERIAL_DEFAULT: 3 On Sabre QEMU: ./simulate: qemu-system-arm -machine sabrelite -nographic -serial null -serial mon:stdio -m size=1024M -kernel images/capdl-loader-image- arm-imx6 ELF-loader started on CPU: ARM Ltd. Cortex-A9 r0p0 paddr=[106fc000..10aa98e3] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 107fe33c. Loaded DTB from 107fe33c. paddr=[1003d000..10047fff] ELF-loading image 'kernel' to 10000000 paddr=[10000000..1003cfff] vaddr=[e0000000..e003cfff] virt_entry=e0000000 ELF-loading image 'capdl-loader' to 10048000 paddr=[10048000..10300fff] vaddr=[10000..2c8fff] virt_entry=187f8 Enabling 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 pre_init@serial.c:501 About to init port, io_ops=0x69cf0 ps_cdev_init@chardev.c:45 About to init_fn 1 ps_cdev_init@chardev.c:46 dev_defn[1].paddr: 0x21e8000, size 1000 uart_init@serial.c:224 about to chardev_map: dev=0x7f8c8, defn->id=1, defn->paddr=0x21e8000 chardev_map@chardev.h:26 ops->io_mapper=0x69cf0 &(ops->io_mapper)=0x1f328 dev->paddr=0x1f654 dev->size=0x4ebc4 uart_init@serial.c:226 chardev_map mapped vaddr 0xbb000 pollcli: Hello Serial Server! pollcli: abc This has me confused - it's good it works, but I can't follow in the flow how the paddr gets changed from the value supplied to chardev_map (ie 0x21e80000 becomes 0x1f654), yet in that case it works. Or is it a complication of using QEMU? A similar kind of test with AOS on odroidc4 - particularly the success of "*uart_init@uart.c:35 Mapped uart paddr:ff803000 size:1000 vaddr:b0000000*" ## Starting application at 0x01080000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A55 r1p0 paddr=[88a000..c2b10f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 9f3068. Loaded DTB from 9f3068. paddr=[247000..252fff] ELF-loading image 'kernel' to 0 paddr=[0..246fff] vaddr=[ffffff8000000000..ffffff8000246fff] virt_entry=ffffff8000000000 ELF-loading image 'sos' to 253000 paddr=[253000..48cfff] vaddr=[400000..639fff] virt_entry=4172e0 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space SOS Starting... <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> uart_init@uart.c:35 Mapped uart paddr:ff803000 size:1000 vaddr:b0000000 SOS Started! test_cspace@tests.c:59 Test cspace run_tests@tests.c:174 Root CSpace test passed! test_cspace@tests.c:59 Test cspace run_tests@tests.c:182 Single level cspace test passed! test_cspace@tests.c:59 Test cspace cspace_alloc_slot@cspace.c:335 Cspace is full! run_tests@tests.c:195 Double level cspace test passed! run_tests@tests.c:199 DMA test passed! run_tests@tests.c:203 Frame table test passed! Network init dwmac.b0002000 Waiting for PHY auto negotiation to complete........ done Speed: 1000, full duplex Protocol ethernet registered (layer: 2). Protocol ipv4 registered (layer: 3). Protocol ipv6 registered (layer: 3). Protocol icmp4 registered (layer: 4). Protocol icmp6 registered (layer: 4). Protocol igmp registered (layer: 4). Protocol udp registered (layer: 4). Protocol tcp registered (layer: 4). Assigned ipv4 0.0.0.0 to device sos picotcp DHCP client: update link Assigned ipv4 192.168.200.125 to device sos picotcp DHCP client: renewal time (T1) 43200 DHCP client: rebinding time (T2) 75600 DHCP client: lease time 86400 DHCP client: netmask 255.255.255.0 DHCP client: gateway 192.168.200.4 Timer init Start first process Starting ttytest at 0x4001c8 SOS entering syscall loop aos: Error attempting syscall 29 task: Hello world, I'm tty_test! handle_syscall@main.c:128 Unknown syscall 1 <<seL4(CPU 0) [receiveIPC/148 T0xffffff803fff8400 "SOS:root" @407a48]: Reply obj ect already has unexecuted reply!>> In this case it has worked, sos_map_device works as expected (although the spurious interrupts are another task to figure out). But trying to understand what's really going on underneath ps_io_map and ultimately why libplatsupport won't work for me has got me confused. Any ideas would be appreciated. Regards Rob

2 4

camkes-vm-linux kernel example
by Hugo V.C. 01 Jul '21

01 Jul '21

Hi, just a simple question: why this tutorial: https://docs.sel4.systems/Tutorials/camkes-vm-linux.html shows this output: Welcome to Buildroot buildroot login: root Password: # grep poke /proc/devices # figure out the major number of our driver 244 poke # mknod /dev/poke c 244 0 # create the special file # echo > /dev/poke # write to the file [ 57.389643] hi -sh: write error: Bad address # the shell complains, but our module is being invoked! I'm not getting the shell complain error, just this: # grep poke /proc/devices 247 poke # mknod /dev/poke c 247 0 # echo > /dev/poke [ 138.946905] TOC TOC NEO... # FYI: my kernel is a custom compiled one but same version as the pre-compiled you provide: # uname -a Linux buildroot 4.9.189 #4 SMP Thu Jun 24 00:16:49 CEST 2021 aarch64 GNU/Linux Any hint? Cheers,

2 2

How will drivers work?
by Isaac Beckett 01 Jul '21

01 Jul '21

Hello! Operating system noob here, I understand that in most mainstream operating systems (Linux, BSDs, MacOS, Windows) drivers are part of the kernel. And in micro kernel operating systems like Minix and seL4, drivers are part of user space. But Minix is a lot closer to a traditional POSIX kernel, and seems to implement some of that (IE posix threads, IPC) in the kernel, which makes the environment for a driver programmer a bit more familiar. How do drivers work in seL4, then? How does a driver obtain permission for hardware access from the kernel? I imagine it works with a capability delegated by the root task, but how do you solve chicken and the egg type problems, like loading driver code, without driver code already loaded? Is it an initramfs like Linux/Unix? Also, what if seL4 is being used _as_ the firmware/bootloader? Obviously it can load the seL4 kernel and user space OS components from a file system to put them in the booting OS’ memory, but how does it load drivers for itself? I’m assuming there’s some low level platform specific code, but is that code verified or part of the proofs?

2 1