April 2020 - 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

Trouble accessing linux guest through tun/tap
by Travis Wheatley 22 May '20

22 May '20

Greetings, I am working with the camkes-arm-vm qemu-arm-virt configuration. I started with the vm_minimal configuration and have added a tun/tap interface by creating the tap on my host thusly: # ip tuntap add tap0 mode tap # ip addr add 10.0.120.100/24 dev tap0 # ip link set dev tap0 up I have added support for what I beleive to be the appropriate interrupts by modifying my devices.camkes file thusly: 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]; Additionally, I have modified the settings.camkes thusly: if(${PLATFORM} STREQUAL "qemu-arm-virt") # force cpu set(QEMU_MEMORY "2048") set(KernelArmCPU cortex-a53 CACHE STRING "" FORCE) set(VmInitRdFile ON CACHE BOOL "" FORCE) set(VmPCISupport ON CACHE BOOL "" FORCE) set(VmVirtioNetArping OFF CACHE BOOL "" FORCE) set(VmVirtioNetVirtqueue ON CACHE BOOL "" FORCE) # set(qemu_sim_extra_args "-netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01") set(qemu_sim_extra_args "-net nic,model=e1000 -netdev tap,id=mynet0,script=no,ifname=tap0 -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01") set(KernelArmExportPCNTUser ON CACHE BOOL "" FORCE) set(KernelArmExportPTMRUser ON CACHE BOOL "" FORCE) endif() This results in a tunl0 interface showing up on my linux guest. However, that interface does not have a mac address associated with it. I can use ifconfig to assign an IP address on the same subnet as the corresponding tap interface on the host. However, I can’t ping between the two. I thought this might be because I have VmVitruoNetArping set to OFF. However, I get compile time errors when I turn it on. Because the tunl0 inteface does not have the mac address specied in the qemu_sim_extra_args I am unsure of how to set up an arp table entry. Exctly what do I need to do to enable network communications between my linux guest and the host?

2 1

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