February 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

Failed to find device frame in new verion on my environment
by yadong.li 16 Apr '20

16 Apr '20

Hi， I recently move my wrok to a new seL4 version (I checkout default.xml in project camkes-arm-vm on 2020.02.25), I have below error print: “create_object@main.c:659 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0x90006000” 1、 I debug code, /**/ is my environment run parameter BOOT_CODE bool_t create_device_untypeds(cap_t root_cnode_cap, seL4_SlotPos slot_pos_before) { paddr_t start = 0; /*---------------------add region, start = 0x1800000, end = 0x2080000 *---------------------add region, start = 0x20ff000, end = 0x2100000 *---------------------add region, start = 0x80000000, end = 0x90001000 *---------------------add region, start = 0x90003000, end = 0x90004000 */ for (word_t i = 0; i < ndks_boot.resv_count; i++) { if (start < ndks_boot.reserved[i].start) { region_t reg = paddr_to_pptr_reg((p_region_t) { start, ndks_boot.reserved[i].start }); if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) { return false; } } start = ndks_boot.reserved[i].end; } /*---------------------add region, start = 0x90005000, CONFIG_PADDR_USER_DEVICE_TOP = 0xff, PPTR_TOP = 0xffffc0000000*/ if (start < CONFIG_PADDR_USER_DEVICE_TOP) { region_t reg = paddr_to_pptr_reg((p_region_t) { start, CONFIG_PADDR_USER_DEVICE_TOP }); /* * The auto-generated bitfield code will get upset if the * end pptr is larger than the maximum pointer size for this architecture. */ if (reg.end > PPTR_TOP) { reg.end = PPTR_TOP; } if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) { return false; } } return true; } 2、 CONFIG_PADDR_USER_DEVICE_TOP = 0xff, I found print the value must use 0x%x, can’t use 0x%lx, it is wrong 3、My platform is cortexA53 kernel/src/plat/j2/config.cmake:28: set(KernelArmCortexA53 ON) 4、and I change follow KernelArmCortexA53： a) ‘math(EXPR KernelPaddrUserTop "(1 << 40) - 1")’ to ‘set(KernelPaddrUserTop "1099511627775")’ ----------the print is “Failed to find device frame” disappear 5、my pc tools install，follow the seL4 wiki， cmakes version is 3.12.2 (> 3.7.2) 6、I did not find error or warning when I ../init-build.sh -DAARCH64=TRUE …… ---------------is it need to install new tools? Or other problem Thank you very much.

2 1

RPi4: DTS memory device and vm_minimal
by Turner, Ben 16 Apr '20

16 Apr '20

Hi, I have been attempting to get the vm_minimal application running on the Raspberry Pi 4 platform, and I have managed to get to the point where I need to define the memory regions for the kernel and virtual machine. The issue is that I do not know what the correct values (if any) would be needed in the overlay-rpi4.dts that I have created. From what I have found to this point, the Pi platform implements a memory system that means it is not possible to define memory regions in a DTS file. These memory regions are user-defined and are not known until runtime. I think I know what the answer will be to this; is there a way to overcome the oddities of the RPi4 memory setup when attempting to create a seL4 CAmkES VM linux image? Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner(a)roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

2 3

Using sel4.xml/sel4arch.xml to generate custom bindings
by Alexandre Mutel 12 Mar '20

12 Mar '20

Hello, I would like to use the sel4.xml API description files to generate custom bindings for a prototype language to interact directly with seL4 without going through libsel4 C API. I assume that the structure of these files could change, which I'm willing to accept, but wanted to know if these files are here to stay in the future? I understand also that I will still have to parse libsel4 C headers to recover the full API which I'm fine with too. Do you see any trouble following this approach or would you recommend something else?

2 1

L4 Risc-v touchscreen board
by Luca Tapponi 27 Feb '20

27 Feb '20

I am newby in this sector and involved in a project to create a prototype (hardware and software) based on risc-v cpu and running L4-based microkernel. I need to control and program an attached touchscreen where I can create a simple graphic user interface too. I would appreciate any suggestion that bring me on the right road. Board should embed wi-fi network too. First step is to find the right hardware and second is to have development tools/environment to program the board. As much as possible open licensing should be adopted because the project falls in IT security solution and want to avoid any hidden backdoors. Thank you in advance. Best regards, Luca

1 0

devices.camkes: vm#.untyped_mmios: What does the integer after the addresses in this array represent?
by Turner, Ben 26 Feb '20

26 Feb '20

Hi all, As stated in the question, I'm not certain about how the integer part of the elements in the untyped_mmios array in devices.camkes are derived? E.g. in the TX2 devices.camkes file: vm0.untyped_mmios = [ "0x3886000:12", // GICV Iface. /* The purpose of these untyped regions is to force the untyped * allocator to treat this memory region as reserved so that when we * try to ensure that the VMM is placed into this region in RAM, it * will definitely be available for placement. * * This address pertains to guest-vm@f1000000 in the overlay DTS */ "0xF1000000:24", "0xF2000000:25", "0xF4000000:26", "0xF8000000:24", ]; I recognise that the range of addresses here covers the VM_RAM_SIZE specified, and so the pattern that emerges is: 24 --> 0x01000000 25 --> 0x02000000 26 --> 0x04000000 And so the above would cover the range 0xf1000000 --> 0xf9000000, which is the range of memory specified for the VM. Is this simply a case of the integer representing double the value with each increment. E.g: Integer Int Rep Hex 0 1 0x0000_0001 1 2 0x0000_0002 2 4 0x0000_0004 3 8 0x0000_0008 4 16 0x0000_0010 5 32 0x0000_0020 6 64 0x0000_0040 7 128 0x0000_0080 8 256 0x0000_0100 9 512 0x0000_0200 10 1024 0x0000_0400 11 2048 0x0000_0800 12 4096 0x0000_1000 13 8192 0x0000_2000 14 16384 0x0000_4000 15 32768 0x0000_8000 16 65536 0x0001_0000 17 131072 0x0002_0000 18 262144 0x0004_0000 19 524288 0x0008_0000 20 1E+06 0x0010_0000 21 2E+06 0x0020_0000 22 4E+06 0x0040_0000 23 8E+06 0x0080_0000 24 2E+07 0x0100_0000 25 3E+07 0x0200_0000 26 7E+07 0x0400_0000 27 1E+08 0x0800_0000 28 3E+08 0x1000_0000 29 5E+08 0x2000_0000 30 1E+09 0x4000_0000 31 2E+09 0x8000_0000 Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner(a)roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

3 2

two questions when I add virtio net with virtio_console meanwhile in arm-vm project
by yadong.li 24 Feb '20

24 Feb '20

hi, I had make virtio_console work OK on my environment（armv8）, But I meet two question when I add virtio net with virtio_console meanwhile. Question1: "add_io_port_range@io.c:111 Requested ioport range 0x6200-0x6600" for VIRTIO CON overlaps with existing range 0x6200-0x6600 for VIRTIO PCI NET According to the print above: common_make_virtio_con(virtio_emul_vm, vm->pci, vm->io_port, VIRTIO_IOPORT_START, VIRTIO_IOPORT_SIZE, VIRTIO_INTERRUPT_PIN, VIRTIO_CON_PLAT_INTERRUPT_LINE, backend); common_make_virtio_net(virtio_emul_vm, vm->pci, vm->io_port, VIRTIO_IOPORT_START + 0x1000, VIRTIO_IOPORT_SIZE, VIRTIO_INTERRUPT_PIN, VIRTIO_NET_PLAT_INTERRUPT_LINE, backend); a、above two function，I found they use the same VIRTIO_IOPORT_START， I modify VIRTIO_IOPORT_START of common_make_virtio_net to （VIRTIO_IOPORT_START + 0x1000）, is it OK? b、I also found（VIRTIO_CON_PLAT_INTERRUPT_LINE == VIRTIO_NET_PLAT_INTERRUPT_LINE）,is that OK? Whether it should be make interrupt line different ? Question2: "_utspace_split_alloc@split.c:272 Failed to find any untyped capable of creating an object at address 0xc0001000 Failed to find device cap for 0xc0001000" According to the print above: a、my PCI region define as below: #define PCI_CFG_REGION_ADDR 0xC1000000 #define PCI_IO_REGION_ADDR 0xC0000000 #define PCI_CFG_REGION_SIZE 0x1000000 #define PCI_IO_REGION_SIZE 0x1000 #define PCI_CFG_BAR_MASK 0xFFFFFFFF I found 'virtio_net_init' and 'virtio_console_init' will call the same function 'install_virtio_vpci_device', net and console will have the same PCI_IO_REGION_ADDR ? is it OK? b、If I want to support two or muti virtio device, which should I add a new macro define for virtio_net in a? for example add PCI_IO_REGION_ADDR for net or add PCI_CFG_REGION_ADDR ? c、Can you give me some list file to change for support for support net and console meanwhile? Thank you very much.

2 2

Adding Platform Support: CAmkES-ARM-VM: VM_Minimal: Raspberry Pi 3b
by Turner, Ben 21 Feb '20

21 Feb '20

Hi, I have been attempting to add support for the Raspberry Pi 3 b platform so that I can run the vm_minimal application on it. The platform supports ARM_HYP, so I believe it should be possible to get this working. I have reached to point where ninja errors on an implicit declaration for `set_gic_vcpu_ctrl_hcr`. From what I understand, this is to do with the ARM Generic Interrupt Controller, however the RPi3b doesn't have a GIC, it has a `bcm2836-armctrl-ic`. This occurs because the file vcpu.h defines an inline function that calls this function, however as the RPi3b doesn't have a GIC, neither the gic_v2.h or gic_v3.h files are provided in the build environment, and hence the build fails. I am unsure what this means in terms of implementation. What needs to be added or changed to get this compiling for the RPi3b? Thanks in advance Ben Turner ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

3 9