- Devel - lists.sel4.systems

additional: some question about VisualCAmkES ？
by yadong.li 27 Apr '20

27 Apr '20

Hi， I found the VisualCAmkES tool can not parse grammar like import and marco in cmakes file, If I write very simple camkes file, only include one assembly and component. I want to know How can I use this VisualCAmkES tool to generate visual file in complex project like vm_minimal ? 发件人: yadong.li 发送时间: 2020年4月25日 21:06 收件人: 'devel(a)sel4.systems' 主题: some question about VisualCAmkES ？ Hi， I want to use VisualCAmkES for view，I follow the step of https://docs.sel4.systems/projects/camkes/visual-camkes/ I meet the below Problem， how can I resolve it ？ Thank you very much Syntax Error (u'/home/yadong.li/seL4_vm_11/ sel4_horizon/camkes-arm-vm/projects/vm/ apps/vm_cross_connector/vm_cross_connector.camkes:36:5: \x1b[31m\ x1b[1mVM_INIT_DEF\x1b[0m()', u' ', u"Syntax error in input at 'VM_INIT_DEF' (type ID) line 36 col 5", u"Syntax error in input at 'VM_GENERAL_COMPOSITION_DEF' (type ID) line 45 col 9", u"Syntax error in input at '(' (type _ANON_4) line 60 col 37")

1 0

some question about VisualCAmkES ？
by yadong.li 25 Apr '20

25 Apr '20

Hi， I want to use VisualCAmkES for view，I follow the step of https://docs.sel4.systems/projects/camkes/visual-camkes/ I meet the below Problem， how can I resolve it ？ Thank you very much Syntax Error (u'/home/yadong.li/seL4_vm_11/ sel4_horizon/camkes-arm-vm/projects/vm/ apps/vm_cross_connector/vm_cross_connector.camkes:36:5: \x1b[31m\ x1b[1mVM_INIT_DEF\x1b[0m()', u' ', u"Syntax error in input at 'VM_INIT_DEF' (type ID) line 36 col 5", u"Syntax error in input at 'VM_GENERAL_COMPOSITION_DEF' (type ID) line 45 col 9", u"Syntax error in input at '(' (type _ANON_4) line 60 col 37")

1 0

Re: [seL4] Trouble with the tun/tap interface in linux guest
by Travis Wheatley 23 Apr '20

23 Apr '20

Thank you for your reply Kent. I modified the devices.camkes in the corresponding project folder as suggested. However, I am still seeing the same behavior. Are there other items I need to add or is there something in the kernel that needs to be enabled? I tried swapping in an Ubuntu server 18.01 kernel. It boots, but I do not even see the tunl0 interface that I see when I boot the default vm_minimal image. Here is what the vm0.untyped_mmios block looks like in my devices.camakes file looks like vm0.untyped_mmios = [ "0x8040000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view) "0x10040000:17", // QEMU PCI MMIO "0x3eff0000:16", // QEMU PCI IO ports "0x40000000:29", // Linux kernel memory regions ]; vm0.dtb_irqs = [35, 36, 37, 38]; I found that the vm_multi project devices.camkes has similar stanzas in the vm0.untyped.mmios block. However, the Interrupt controller item has an additional 0x1000 token in it: "0x8040000:0x1000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view) I tried this in the vm_minimal configurationo but ../init.sh throws an error indicating that it doesn’t know how to parse that. I also was able to boot the vm_multi configuration in the emulator and noticed that it did, in fact, have both an eth0 and eth1 interface, but was not able to get them to work because the kernel seemed to be stuck in a loop looking for a non-existent DHCP server. Wondering if there is some other config somewhere that I need to get a working eth0 interface on the vm_minimal configuration? Message: 1 Date: Tue, 21 Apr 2020 20:57:24 +0000 From: Travis Wheatley <travis.wheatley(a)emergentspace.com<mailto:travis.wheatley@emergentspace.com>> To: "devel(a)sel4.systems<mailto:devel@sel4.systems>" <devel(a)sel4.systems<mailto:devel@sel4.systems>> Subject: [seL4] Trouble with the tun/tap interface in linux guest Message-ID: <207FF441-86A1-4CE3-88AD-8BACC908138D(a)emergentspace.com<mailto:207FF441-86A1-4CE3-88AD-8BACC908138D@emergentspace.com>> Content-Type: text/plain; charset="utf-8" Thanks to recent patches I have been able to build and boot the linux guest kernel under the simulator in the camkes-arm-vm project using the vm_minimal configuration. However, I am having trouble accessing it via the network interface. First I set up a tap interface as follows: # sudo ip tuntap add tap0 mode tap # sudo ip addr add 10.0.120.100/24 dev tap0 # sudo ip link set dev tap0 up Then I start the simulation using the following command line, which I believe should make the tap interface appear as an e1000 nic to the guest kernel: ./simulate --extra-qemu-args="-net nic,model=e1000 -net tap,script=no,ifname=tap0? In the linux guest the ?ip a? command shows that there is a tunl0 network device available. I have tried a couple of methods of activating it including using ifconfig to bring it up and assign it an ip address as well as the ?ip link set tun0 up? followed by the ?ip addr add 10.0.120.1/24 dev tunl0? command. According to ifconfig both of these bring the interface up and provide it with an ip address. However, I can?t ping the tap ip address from the guest nor can I ping the guest tunl0 interface from another console on the host. So, what am I missing? ------------------------------ Message: 2 Date: Tue, 21 Apr 2020 23:09:16 +0000 From: "Mcleod, Kent (Data61, Kensington NSW)" <Re: [seL4] Trouble with the tun/tap interface in linux guest> To: Travis Wheatley <travis.wheatley(a)emergentspace.com<mailto:travis.wheatley@emergentspace.com>>, "devel(a)sel4.systems<mailto:devel@sel4.systems>" <devel(a)sel4.systems<mailto:devel@sel4.systems>> Subject: Re: [seL4] Trouble with the tun/tap interface in linux guest Message-ID: <SYXPR01MB0832783D9CD6B3B03B0F04FFABD50(a)SYXPR01MB0832.ausprd01.prod.outlook.com<mailto:SYXPR01MB0832783D9CD6B3B03B0F04FFABD50@SYXPR01MB0832.ausprd01.prod.outlook.com>> Content-Type: text/plain; charset="iso-8859-1" It could be that the camkes configuration doesn't pass through the PCI device to the Linux guest? You need to add the Interrupts and PCI MMIO configurations below: ? ? ? ? vm0.untyped_mmios = [ ? ? ? ? ? ? ? ? ? ? "0x8040000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view) ? ? ? ? ? ? ? ? ? ? "0x10040000:17", // QEMU PCI MMIO ? ? ? ? ? ? ? ? ? ? "0x3eff0000:16", // QEMU PCI IO ports ? ? ? ? ? ? ? ? ? ? "0x40000000:29", // Linux kernel memory regions ? ? ? ? ? ? ? ? ? ? ]; ? ? ? ? vm0.dtb_irqs = ?[35, 36, 37, 38]; The device should then appear in the guest under eth0. Kent. ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 71, Issue 24 *************************************

1 0

Trouble with the tun/tap interface in linux guest
by Travis Wheatley 22 Apr '20

22 Apr '20

Thanks to recent patches I have been able to build and boot the linux guest kernel under the simulator in the camkes-arm-vm project using the vm_minimal configuration. However, I am having trouble accessing it via the network interface. First I set up a tap interface as follows: # sudo ip tuntap add tap0 mode tap # sudo ip addr add 10.0.120.100/24 dev tap0 # sudo ip link set dev tap0 up Then I start the simulation using the following command line, which I believe should make the tap interface appear as an e1000 nic to the guest kernel: ./simulate --extra-qemu-args="-net nic,model=e1000 -net tap,script=no,ifname=tap0” In the linux guest the “ip a” command shows that there is a tunl0 network device available. I have tried a couple of methods of activating it including using ifconfig to bring it up and assign it an ip address as well as the “ip link set tun0 up” followed by the “ip addr add 10.0.120.1/24 dev tunl0” command. According to ifconfig both of these bring the interface up and provide it with an ip address. However, I can’t ping the tap ip address from the guest nor can I ping the guest tunl0 interface from another console on the host. So, what am I missing?

2 1

Incorporating the Build System - The CAmkES Perspective
by Turner, Ben 21 Apr '20

21 Apr '20

Hi, We are attempting to define a system that comprises 3 components that can talk to each other. We have managed to get the system built and working using the existing tutorial repo and the hello-camkes-0 app, however we are struggling to determine what precisely we would need to copy from this in order to define our own standalone application within the seL4 build system. We have read the existing documentation at https://docs.sel4.systems/projects/buildsystem/incorporating.html but cannot find any information on what additions are required when using the CAmkES and ARM capabilities. Any help you can provide would be appreciated. Kind regards, 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. ________________________________________

2 1

TimeServer "IRQ already mapped" error
by Grant Jurgensen 17 Apr '20

17 Apr '20

Hi all, I'm trying to add a timer to my CAmkES component (all I need is a timestamp). I've been using this example component as a reference: https://github.com/seL4/camkes/tree/master/apps/timeserver My problem is that when I declare an instance of the global TimeServer component in my ".camkes" file, I get an error at build-time: "parse-capDL: IRQ already mapped: 68". I'm not sure what to make of this error. The only major difference between my project and the reference above is that I am building atop the camkes-arm-vm project. Could the VM be interfering here? Thanks, Grant Jurgensen

2 3

Benchmarks of seL4
by Leo Gaspard 16 Apr '20

16 Apr '20

Hello, I come wondering: the FAQ claims that seL4 is “the world's fastest microkernel”. However, I can only find benchmarks of just seL4, without comparison to other operating systems running on the same machine. Would you happen to have such comparative benchmarks? I'd be particularly interested by something against L4Re, as it'd probably allow me to guess at the performance of something similar to L4Linux ported to seL4. Thank you for all you do on seL4! Leo

6 12

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

Trouble booting default cmakes-vm-arm project under QEMU
by Travis Wheatley 16 Apr '20

16 Apr '20

Sel4 Developers, Still learning to crawl here. I have built the cmakes-vm-arm project for the qemu-arm-virt target. I have QEMU version 3.1.0 installed on my host. When I run the simulation by executing the command “./simulate”. it appears as though Sel4 is booting and successfully downloading the kernel, dtb, and loader. However, I am running into problems when it starts booting the kernel. It looks to me like it might be booting the kernel OK with the exception of a warning about GIC interrupts and subsequently drops to user space. Following that I see errors about insufficient memory and invalid num_vcpus. Not quite sure how to correct this. Hoping one of y’all can point me in the right direction. Here is a copy of the output — Begin included text — $ ./simulate ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61b01000..62edd947] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61bf7400. Loaded DTB from 61bf7400. paddr=[60239000..6023afff] ELF-loading image 'kernel' paddr=[60000000..60238fff] vaddr=[ff8060000000..ff8060238fff] (my_virtual_env) trickdev@trickvm ~/cmakes-arm-vm/vm-build $ ./simulate ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61b01000..62edd947] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61bf7400. Loaded DTB from 61bf7400. paddr=[60239000..6023afff] ELF-loading image 'kernel' paddr=[60000000..60238fff] vaddr=[ff8060000000..ff8060238fff] virt_entry=ff8060000000 ELF-loading image 'capdl-loader' paddr=[6023b000..61703fff] vaddr=[400000..18c8fff] virt_entry=407fe8 Enabling hypervisor 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 <<seL4(CPU 0) [decodeUntypedInvocation/216 T0xff80bf815400 "rootserver" @400704]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> run(a)main.c<mailto:run@main.c>:1095 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1) sel4platsupport_copy_irq_cap(a)device.c<mailto:sel4platsupport_copy_irq_cap@device.c>:41 Failed to get cap for irq irq_register_common(a)irq.c<mailto:irq_register_common@irq.c>:316 Failed to register an IRQ Assertion failed: (cspace->bitmap[index / BITS_PER_WORD] & BIT(index % BITS_PER_WORD)) == 0 (/home/trickdev/cmakes-arm-vm/projects/seL4_libs/libsel4allocman/src/cspace/single_level.c: _cspace_single_level_free: 100)

2 1