- Devel - lists.sel4.systems

CAmkES Linux VM Tutorial/Minimal Build Issue
by Jim McColl 15 Sep '20

15 Sep '20

So there I was having a lovely time doing the seL4 Tutorials...and I got hit with debug output #1 below, so I confirmed that I indeed had nested virtualization working by making an running an Ubuntu VM in side of an Ubuntu VM on an Ubuntu box in using kvm and qemu, so I do not think it is that. I tried passing the host processor through just to see if there something was getting in the way to no avail. That was when I decided to go through the devel archives and the closest similar post I could find was 07 Aug 2020 ( https://sel4.systems/pipermail/devel/2020-August/002845.html) unfortunately there's no debug output so I cannot confirm is it is the same issue. There was also an issue in April ( https://sel4.systems/pipermail/devel/2020-April/002781.html) that also looked similar but I grep'd through the source and could not find the line referenced line from the commit. Finally I natively built minimal from https://github.com/seL4/camkes-vm-examples in the hopes that it was an issue with the tutorial docker container which led to output #2 below. Which brings me to now humbly request for help so I can finish up the tutorials. Thank you advance for any help anyone can provide, hopefully it is a simple mistake on my part. -Jim ====== VERY LONG DEBUG STUFF BELOW ====== - Debug Output #1: ./simulate: 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 -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 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xa1d000 end=0x1e366e0 size=0x14196e0 name='images/capdl-loader-image-x86_64-pc99' Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 7fedf000 type 1 Adding physical memory region 0x100000-0x7ffdf000 Physical Memory Region from 7ffdf000 size 21000 type 2 Physical Memory Region from b0000000 size 10000000 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from feffc000 size 4000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Multiboot gave us no video information ACPI: RSDP paddr=0xf68d0 ACPI: RSDP vaddr=0xf68d0 ACPI: RSDT paddr=0x7ffe210d ACPI: RSDT vaddr=0x7ffe210d Kernel loaded to: start=0x100000 end=0xa1c000 size=0x91c000 entry=0x10125e ACPI: RSDT paddr=0x7ffe210d ACPI: RSDT vaddr=0x7ffe210d ACPI: FADT paddr=0x7ffe1ee5 ACPI: FADT vaddr=0x7ffe1ee5 ACPI: FADT flags=0x84a5 ACPI: DMAR paddr=0x7ffe20c5 ACPI: DMAR vaddr=0x7ffe20c5 ACPI: IOMMU host address width: 39 ACPI: 1 IOMMUs detected ACPI: MADT paddr=0x7ffe1fd9 ACPI: MADT vaddr=0x7ffe1fd9 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: size=0x289a000 v_entry=0x4083af v_start=0x400000 v_end=0x2c9a000 p_start=0x1e37000 p_end=0x46d1000 Moving loaded userland images to final location: from=0x1e37000 to=0xa1c000 size=0x289a000 Starting node #0 with APIC ID 0 Mapping kernel window is done vt-x: Load IA32_PERF_GLOBAL_CONTROL not supported. Hardware debugging may not work IOMMU 0x0: 16-bit domain IDs supported IOMMU: Using 3 page-table levels (max. supported:3) IOMMU: Create VTD context table for PCI bus 0x0 (pptr=0xffffff807e01d000) ===== SNIP ====== IOMMU: Create VTD context table for PCI bus 0xfe (pptr=0xffffff807e11b000) IOMMU: Create VTD context table for PCI bus 0xff (pptr=0xffffff807e11c000) IOMMU 0x0: enabling... enabled Booting all finished, dropped to user space Single bus detected lib_pci_scan_dev found pci device 0 0 PCI :: 00.00.00 : intel Unknown device ID. (vid 0x8086 did 0x29c0) line0 pin0 lib_pci_scan_dev found pci device 0 1 PCI :: 00.01.00 : Unknown vendor ID. Unknown device ID. (vid 0x1234 did 0x1111) line0 pin0 BAR0 : [ mem 0xfd000000 sz 0x1000000 szmask 0xff000000 prefetch ] BAR2 : [ mem 0xfebb0000 sz 0x1000 szmask 0xfffff000 ] lib_pci_scan_dev found pci device 0 2 PCI :: 00.02.00 : intel Unknown device ID. (vid 0x8086 did 0x100e) line11 pin1 BAR0 : [ mem 0xfeb80000 sz 0x20000 szmask 0xfffe0000 ] BAR1 : [ io 0xc000 sz 0x40 szmask 0xffffffc0 ] lib_pci_scan_dev found pci device 0 31 PCI :: 00.1f.00 : intel intel_ich9_8 (vid 0x8086 did 0x2918) line0 pin0 lib_pci_scan_dev found multi function device 0 31 PCI :: 00.1f.02 : intel Unknown device ID. (vid 0x8086 did 0x2922) line10 pin1 BAR4 : [ io 0xc080 sz 0x20 szmask 0xffffffe0 ] BAR5 : [ mem 0xfebb1000 sz 0x1000 szmask 0xfffff000 ] PCI :: 00.1f.03 : intel intel_ich9_6 (vid 0x8086 did 0x2930) line10 pin1 BAR4 : [ io 0x700 sz 0x40 szmask 0xffffffc0 ] ========== KERNEL EXCEPTION ========== Vector: 0xd ErrCode: 0x0 IP: 0xffffffff8080d2e9 SP: 0xffffffff80a0bd88 FLAGS: 0x10002 CR0: 0x8001003b CR2: 0x0 (page-fault address) CR3: 0xa17000 (page-directory physical address) CR4: 0x2220 Stack Dump: *0xffffffff80a0bd88 == 0xffffff807c052880 *0xffffffff80a0bd90 == 0xffffff80318c1400 *0xffffffff80a0bd98 == 0x1 *0xffffffff80a0bda0 == 0xffffffff80812415 *0xffffffff80a0bda8 == 0xffffff8020001580 *0xffffffff80a0bdb0 == 0x1000ff8029831000 *0xffffffff80a0bdb8 == 0xc *0xffffffff80a0bdc0 == 0xffffffff8081eeb8 *0xffffffff80a0bdc8 == 0xc *0xffffffff80a0bdd0 == 0xffffff8020002560 *0xffffffff80a0bdd8 == 0xffffff8029831000 *0xffffffff80a0bde0 == 0x0 *0xffffffff80a0bde8 == 0x1ffed6 *0xffffffff80a0bdf0 == 0xffffff8029831000 *0xffffffff80a0bdf8 == 0xffffff80318c1c00 *0xffffffff80a0be00 == 0xffffff8020002540 *0xffffffff80a0be08 == 0xffffffff80a0be60 *0xffffffff80a0be10 == 0xffffff8020002540 *0xffffffff80a0be18 == 0xffffff80318c18a0 *0xffffffff80a0be20 == 0xffffff8029831000 Halting... halting... Kernel entry via Syscall, number: 1, Call Cap type: 12, Invocation tag: 54 - Debug Output #2: ===== SNIP: Same as above ===== IOMMU: Create VTD context table for PCI bus 0xff (pptr=0xff10d000) IOMMU 0x0: enabling... enabled Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/208 T0xff10e400 "rootserver" @8048495]: Untyped Retype: Insufficient memory (1 * 8388608 bytes needed, 0 bytes available).>> Single bus detected lib_pci_scan_dev found pci device 0 0 PCI :: 00.00.00 : intel Unknown device ID. (vid 0x8086 did 0x29c0) line0 pin0 lib_pci_scan_dev found pci device 0 1 PCI :: 00.01.00 : Unknown vendor ID. Unknown device ID. (vid 0x1234 did 0x1111) line0 pin0 BAR0 : [ mem 0xfd000000 sz 0x1000000 szmask 0xff000000 prefetch ] BAR2 : [ mem 0xfebb0000 sz 0x1000 szmask 0xfffff000 ] lib_pci_scan_dev found pci device 0 2 PCI :: 00.02.00 : intel Unknown device ID. (vid 0x8086 did 0x100e) line11 pin1 BAR0 : [ mem 0xfeb80000 sz 0x20000 szmask 0xfffe0000 ] BAR1 : [ io 0xc000 sz 0x40 szmask 0xffffffc0 ] lib_pci_scan_dev found pci device 0 31 PCI :: 00.1f.00 : intel intel_ich9_8 (vid 0x8086 did 0x2918) line0 pin0 lib_pci_scan_dev found multi function device 0 31 PCI :: 00.1f.02 : intel Unknown device ID. (vid 0x8086 did 0x2922) line10 pin1 BAR4 : [ io 0xc080 sz 0x20 szmask 0xffffffe0 ] BAR5 : [ mem 0xfebb1000 sz 0x1000 szmask 0xfffff000 ] PCI :: 00.1f.03 : intel intel_ich9_6 (vid 0x8086 did 0x2930) line10 pin1 BAR4 : [ io 0x700 sz 0x40 szmask 0xffffffc0 ] seL4 failed assertion '(cte_t *)mdb_node_get_mdbNext(destSlot->cteMDBNode) == NULL && (cte_t *)mdb_node_get_mdbPrev(destSlot->cteMDBNode) == NULL' at /home/user/Documents/labs/rr/os/seL4-AUS/camkes_vm_examples/kernel/src/object/cnode.c:428 in function cteInsert halting... Kernel entry via Syscall, number: 1, Call Cap type: 12, Invocation tag: 53

2 1

Unable to setup Camkes VM tutorial
by Chris Koziarz 11 Sep '20

11 Sep '20

There is something wrong with Camkes VM repo or with my Linux machine. I am able to setup repo of other tutorials, i.e. repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest works. However when I continue into Camkes VM: root@ubuntu:~/lv4_repo# mkdir camkes_VM root@ubuntu:~/lv4_repo# cd camkes_VM root@ubuntu:~/lv4_repo/camkes_VM# repo init -u https://github.com/sel4/camkes-vm-examples-manifest.git -b tipc-stage I get the following error: Downloading Repo source from https://gerrit.googlesource.com/git-repo fatal: Cannot get https://gerrit.googlesource.com/git-repo/clone.bundle fatal: error [Errno -3] Temporary failure in name resolution fatal: cloning the git-repo repository failed, will remove '.repo/repo' What might be going wrong? As can be seen, I'm running on ubuntu v20.04 Any help appreciated. Chris

2 1

seL4 Summit 2020 - Call for Presentations *extended* to Sep 15.
by Kuz, Ihor (Data61, Kensington NSW) 10 Sep '20

10 Sep '20

Hi, For people not on the seL4 announce list: the 3rd annual seL4 Summit will be held online on November 15-18, 2020. A call for presentations is out, and the deadline for submissions has been extended to September 15, 2020. Please consider submitting something about seL4-based work that you are doing or other seL4/microkernel/trustworthy systems topics. Submission only requires a title and abstract, so it’s pretty low overhead. Submit by email to Summit2020(a)sel4-us.org. See more detail on the announce list[1]. Ihor. [1] https://sel4.systems/pipermail/announce/2020/000036.html

1 0

CAmkES Linux VM - Networking
by Cedric MAIRE 03 Sep '20

03 Sep '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

Running RISC-V sel4 in QEMU/Spike
by Porter, Jeremy 02 Sep '20

02 Sep '20

I'm following the steps to build sel4 for QEMU and Spike here: https://docs.sel4.systems/Hardware/spike.html Spike - seL4 Docs | seL4 docs<https://docs.sel4.systems/Hardware/spike.html> If you plan to use the ./simulate script, please be sure to add the -DSIMULATION=1 argument when running cmake. Generated binaries can be found in the images/ directory.. You can also use run the tests on the 32-bit spike platform by replacing the -DRISCV64=TRUE option with -DRISCV32=TRUE. docs.sel4.systems Since my system doesn't have QEMU 4.2 or better I built the latest version of QEMU and use that instead. I get the following error from QEMU: /mnt/data/qemu/build/riscv64-softmmu/qemu-system-riscv64 -machine spike -nographic -serial mon:stdio -m size=4095M -kernel images/sel4test-driver-image-riscv-spikeqemu-system-riscv64: Unable to load the RISC-V firmware "opensbi-riscv64-spike-fw_jump.elf" In Spike this happens: /mnt/data/rocket-tools/bin/spike images/sel4test-driver-image-riscv-spike bbl loader ELF-loader started on (HART 0) (NODES 1) paddr=[80200000..8064d4d7] Looking for DTB in CPIO archive...found at 802cb1a0. Loaded DTB from 802cb1a0. paddr=[8402a000..8402afff] ELF-loading image 'kernel' paddr=[84000000..84029fff] vaddr=[ffffffff84000000..ffffffff84029fff] virt_entry=ffffffff84000000 ELF-loading image 'sel4test-driver' paddr=[8402b000..84401fff] vaddr=[10000..3e6fff] virt_entry=1b540 Jumping to kernel-image entry point... Init local IRQ Initialing PLIC... The tutorials lead me to believe this should go to user space. i.e. 327 printf("Booting all finished, dropped to user space\n"); in kernel/src/arch/riscv/kernel/boot.c Can anyone point out what's going wrong here in these two cases? Thank you! Jeremy

2 1

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 26 Aug '20

26 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