- Devel - lists.sel4.systems

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

Announcing new releases: seL4-11.0.0, camkes-3.8.0, CapDL-0.1.0,
by Mcleod, Kent (Data61, Kensington NSW) 20 Feb '20

20 Feb '20

Announcing the releases of seL4, CAmkES, CapDL and updates of other supporting projects. **Note that this announcement refers to a series of release commits that occurred on 19-Nov-2019.** See below for links to release notes. In addition there are new ways to discuss seL4 and trustworthy systems: - seL4 Discourse at <https://sel4.discourse.group>, a forum for attempting to build up an seL4 knowledge base. - seL4 Mattermost at <https://mattermost.ts.data61.csiro.au/sel4-external/> for online messaging. (Signup link can be found on seL4 Discourse:<https://sel4.discourse.group/t/sel4-mattermost-sign-up-link/125> with a valid account). - seL4 RFCs at <https://sel4.atlassian.net/projects/RFC> for open discussion about major changes to the seL4 ecosystem. For more information see: <https://docs.sel4.systems/processes/#contact> Versioned Releases * seL4 11.0.0: The seL4 microkernel <https://docs.sel4.systems/releases/sel4/11.0.0> * CAmkES camkes-3.8.0: Component Architecture for microkernel-based Embedded Systems <https://docs.sel4.systems/releases/camkes/camkes-3.8.0> * CapDL 0.1.0: Collection of tools for generating, parsing and loading CapDL specifications of systems <https://docs.sel4.systems/releases/capdl/0.1.0> Update notes * seL4 Buildsystem: System configuration and building using mostly CMake <https://docs.sel4.systems/updates/buildsystem/11.0.x.html> * seL4Test: Test suite for seL4 <https://docs.sel4.systems/updates/sel4test/11.0.x.html> * sel4bench: sel4bench contains benchmarking applications and a support library for seL4 <https://docs.sel4.systems/updates/sel4bench/11.0.x.html> * user_libs: Userlevel libraries on seL4 <https://docs.sel4.systems/updates/user_libs/11.0.x.html> * The seL4 Run-time: A minimal runtime for running a C or C-compatible process in a minimal seL4 environment <https://docs.sel4.systems/updates/sel4runtime/11.0.x.html> * Elfloader: For preparing the hardware for seL4 on ARM and RISC-V <https://docs.sel4.systems/updates/elfloader/11.0.x.html> * seL4 tutorials: Collection of tutorials for learning to use seL4 and its ecosystem <https://docs.sel4.systems/updates/sel4-tutorials/camkes-3.8.x.html> * camkes-vm: x86 Virtual Machine build as a CAmkES component <https://docs.sel4.systems/updates/camkes-vm/camkes-3.8.x.html> * camkes-arm-vm: Arm Virtual Machine build as a CAmkES component <https://docs.sel4.systems/updates/camkes-arm-vm/camkes-3.8.x.html> * seL4webserver: A reference for implementing applications on seL4 <https://docs.sel4.systems/updates/sel4webserver/camkes-3.8.x.html> An seL4 discourse version of this email can be found at: <https://sel4.discourse.group/t/19-november-2019/126>

1 0

Re: [seL4] Multikernels and resource transfer
by Ge, Qian (Data61, Kensington NSW) 14 Feb '20

14 Feb '20

In a multikernel setup, each kernel manages its own memory allocation, as the main memory is distributed among all valid kernels. Hence, the described scenario does not apply. Regards, Qian. Message: 1 Date: Thu, 13 Feb 2020 00:49:11 -0500 From: Demi Obenour <demiobenour(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] Multikernels and resource transfer Message-ID: <CAJEMUN_L49O9btYx03Z35uQ6S21T80wPujP86Gd5XyymH4BQ6g(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" In a multikernel, how would retyping work? Obviously, the kernel cannot allow untyped X to be used for page tables if user code on another core might still have write access to it. Would retyping involve some sort of in-kernel concurrency? Obviously, the clustered multikernel avoids this, but making applications (as opposed to low-level libraries and services) work around kernel limitations seems rather unappealing. Sincerely, Demi

1 0

Multikernels and resource transfer
by Demi Obenour 13 Feb '20

13 Feb '20

In a multikernel, how would retyping work? Obviously, the kernel cannot allow untyped X to be used for page tables if user code on another core might still have write access to it. Would retyping involve some sort of in-kernel concurrency? Obviously, the clustered multikernel avoids this, but making applications (as opposed to low-level libraries and services) work around kernel limitations seems rather unappealing. Sincerely, Demi

1 0

Beginner ARM_HYP questions
by tossel＠gmail.com 11 Feb '20

11 Feb '20

Greetings, I'm trying to understand how hypervisor functionality support is working in seL4 for aarch32/aarch64. In the documentation there is a list of platforms [1] for some of them ARM_HYP is said to be supported for some not. I was trying to grep through the kernel, but it seemed to me that ARM_HYP can be enabled on any ARM-based platform. I've tried to compile sel4test for exynos5422 (for which ARM_HYP is said to be enabled) and odroidc2 (for which it is said that it's not supported) with -DARM_HYP=ON manually set, and for both compilation succeeded. It failed for hikey, that should support it, but that's a different story. So my questions are - How is it defined whether ARM_HYP is supported for a board/SoC, provided that processor architecture supports it? What the platform support code should provide for hypervisor to work? - For platforms not supported by camkes-arm-vm (like, most of the platforms) how ARM_HYP can be tested? Thanks a lot, Anton Gerasimov [1] https://docs.sel4.systems/Hardware/

2 2

(no subject)
by abdi mahmud haji 11 Feb '20

11 Feb '20

hello can someone help me here what did i do wrong ,i have been trying to do camkes-vm-linux and i have followed the instruction on sel4-tutorials when i run ninja to build the file i have got an error as below ========================================================================== ninja [5/127] Building C object camkes-vm-li...ents/Init/src/virtio_net_vswitch.c.obj FAILED: ccache /usr/bin/gcc --sysroot=/home/sel4/sel4-tutorials-manifest/camkes-vm-linux_build -I../projects/camkes/vm/components/Init/src -I../projects/camkes/vm/components/VM/configurations -Icamkes-vm-linux/vm0/include -I../kernel/libsel4/include -I../kernel/libsel4/arch_include/x86 -I../kernel/libsel4/sel4_arch_include/x86_64 -I../kernel/libsel4/sel4_plat_include/pc99 -I../kernel/libsel4/mode_include/64 -Ilibsel4/include -Ilibsel4/arch_include/x86 -Ilibsel4/sel4_arch_include/x86_64 -I../projects/sel4runtime/include -I../projects/sel4runtime/include/mode/64 -I../projects/sel4runtime/include/arch/x86 -I../projects/sel4runtime/include/sel4_arch/x86_64 -Iprojects/musllibc/build-temp/stage/include -Ilibsel4/autoconf -Ikernel/gen_config -Ilibsel4/gen_config -I../tools/camkes/libsel4camkes/include -I../projects/seL4_libs/libsel4debug/include -I../projects/seL4_libs/libsel4debug/arch_include/x86 -I../projects/seL4_libs/libsel4debug/sel4_arch_include/x86_64 -I../projects/util_libs/libutils/include -I../projects/util_libs/libutils/arch_include/x86 -Iprojects/util_libs/libutils/gen_config -I../projects/util_libs/libplatsupport/include -I../projects/util_libs/libplatsupport/plat_include/pc99 -I../projects/util_libs/libplatsupport/arch_include/x86 -Iprojects/util_libs/libplatsupport/gen_config -I../projects/seL4_libs/libsel4muslcsys/include -I../projects/util_libs/libcpio/include -I../projects/seL4_libs/libsel4utils/include -I../projects/seL4_libs/libsel4utils/sel4_arch_include/x86_64 -I../projects/seL4_libs/libsel4utils/arch_include/x86 -I../projects/seL4_libs/libsel4vspace/include -I../projects/seL4_libs/libsel4vspace/arch_include/x86 -I../projects/seL4_libs/libsel4vka/include -I../projects/seL4_libs/libsel4vka/sel4_arch_include/x86_64 -I../projects/seL4_libs/libsel4vka/arch_include/x86 -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -I../projects/seL4_libs/libsel4simple/include -I../projects/seL4_libs/libsel4simple/arch_include/x86 -I../projects/seL4_libs/libsel4platsupport/include -I../projects/seL4_libs/libsel4platsupport/arch_include/x86 -I../projects/seL4_libs/libsel4platsupport/plat_include/pc99 -I../projects/seL4_libs/libsel4simple-default/include -I../projects/util_libs/libelf/include -Iprojects/seL4_libs/libsel4muslcsys/gen_config -I../projects/seL4_libs/libsel4sync/include -I../projects/projects_libs/libvirtqueue/include -Icamkes-vm-linux/libsel4camkes/gen_config -Iprojects/sel4runtime/gen_config -I../projects/seL4_libs/libsel4allocman/include -I../projects/seL4_libs/libsel4allocman/sel4_arch/x86_64 -I../projects/seL4_libs/libsel4allocman/arch/x86 -I../projects/seL4_libs/libsel4vmm/include -I../projects/util_libs/libpci/include -I../projects/util_libs/libethdrivers/include -I../projects/util_libs/libethdrivers/plat_include/pc99 -I../projects/util_libs/libethdrivers/arch_include/x86 -Iprojects/util_libs/libethdrivers/gen_config -Iprojects/util_libs/liblwip/gen_config -Iprojects/util_libs/libpicotcp/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Icamkes-vm-linux/vm/gen_config -I../projects/projects_libs/libvswitch/include -I../projects/camkes/global-components/components/FileServer/libFileServer-client/. -m64 -march=nehalem -D__KERNEL_64__ -g -nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mtls-direct-seg-refs -Wno-main -std=gnu11 -MD -MT camkes-vm-linux/CMakeFiles/vm0.instance.bin.dir/__/projects/camkes/vm/components/Init/src/virtio_net_vswitch.c.obj -MF camkes-vm-linux/CMakeFiles/vm0.instance.bin.dir/__/projects/camkes/vm/components/Init/src/virtio_net_vswitch.c.obj.d -o camkes-vm-linux/CMakeFiles/vm0.instance.bin.dir/__/projects/camkes/vm/components/Init/src/virtio_net_vswitch.c.obj -c ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘virtio_net_notify_vswitch_send’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:50:23: warning: implicit declaration of function ‘virtqueue_driver_dequeue’ [-Wimplicit-function-declaration] int dequeue_res = virtqueue_driver_dequeue(node->virtqueues.send_queue, ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘emul_raw_tx’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:123:13: error: unknown type name ‘virtqueue_t’ virtqueue_t *destbuff; ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:147:19: warning: implicit declaration of function ‘virtqueue_driver_enqueue’ [-Wimplicit-function-declaration] err = virtqueue_driver_enqueue(destnode->virtqueues.send_queue, ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:157:19: warning: implicit declaration of function ‘virtqueue_driver_signal’ [-Wimplicit-function-declaration] err = virtqueue_driver_signal(destnode->virtqueues.send_queue); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:170:17: warning: implicit declaration of function ‘virtqueue_driver_poll’ [-Wimplicit-function-declaration] if (virtqueue_driver_poll(destnode->virtqueues.send_queue) == 1) { ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘virtio_net_notify_vswitch_recv’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:215:5: error: unknown type name ‘virtqueue_t’ virtqueue_t *rxdata_buff; ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:234:23: warning: implicit declaration of function ‘virtqueue_device_dequeue’ [-Wimplicit-function-declaration] int dequeue_res = virtqueue_device_dequeue(node->virtqueues.recv_queue, ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:249:27: warning: implicit declaration of function ‘virtqueue_device_enqueue’ [-Wimplicit-function-declaration] enqueue_res = virtqueue_device_enqueue(node->virtqueues.recv_queue, available_buff, available_buff_sz); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:275:11: warning: implicit declaration of function ‘virtqueue_device_signal’ [-Wimplicit-function-declaration] err = virtqueue_device_signal(node->virtqueues.recv_queue); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘virtio_net_notify_vswitch’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:292:17: warning: implicit declaration of function ‘virtqueue_device_poll’ [-Wimplicit-function-declaration] if (virtqueue_device_poll(g_vswitch.nodes[i].virtqueues.recv_queue) == 1) { ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘make_vswitch_net’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:312:44: warning: passing argument 1 of ‘camkes_virtqueue_driver_init’ from incompatible pointer type [-Wincompatible-pointer-types] err = camkes_virtqueue_driver_init(&send_virtqueue, mac_mapping.send_id); ^ In file included from ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:29:0: ../tools/camkes/libsel4camkes/include/camkes/virtqueue.h:64:5: note: expected ‘virtqueue_driver_t * {aka struct virtqueue_driver *}’ but argument is of type ‘virtqueue_driver_t ** {aka struct virtqueue_driver **}’ int camkes_virtqueue_driver_init(virtqueue_driver_t *driver, unsigned int camkes_virtqueue_id); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:317:44: warning: passing argument 1 of ‘camkes_virtqueue_device_init’ from incompatible pointer type [-Wincompatible-pointer-types] err = camkes_virtqueue_device_init(&recv_virtqueue, mac_mapping.recv_id); ^ In file included from ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:29:0: ../tools/camkes/libsel4camkes/include/camkes/virtqueue.h:72:5: note: expected ‘virtqueue_device_t * {aka struct virtqueue_device *}’ but argument is of type ‘virtqueue_device_t ** {aka struct virtqueue_device **}’ int camkes_virtqueue_device_init(virtqueue_device_t *device, unsigned int camkes_virtqueue_id); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:320:13: warning: implicit declaration of function ‘camkes_virtqueue_driver_free’ [-Wimplicit-function-declaration] camkes_virtqueue_driver_free(send_virtqueue); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:333:13: warning: implicit declaration of function ‘camkes_virtqueue_device_free’ [-Wimplicit-function-declaration] camkes_virtqueue_device_free(recv_virtqueue); ^ [5/127] Building C object camkes-vm-li...MakeFiles/sel4camkes.dir/src/dma.c.obj ninja: build stopped: subcommand failed. ================================================================== and why this happing

2 1

Problem booting camkes arm vmm on TK1 from SD Card
by Mike Clark 10 Feb '20

10 Feb '20

I'm using the docker image to build the CAmkES ARM VMM project using roughly the instructions here: https://docs.sel4.systems/VM/CAmkESARMVM.html (they are slightly out of date). I do: ../init-build.sh -DAARCH32=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tk1 ninja Then I copy the resulting image from the images directory to an SD card and put that in my TK1. When U-Boot starts I use the following commands to try to boot fatload mmc 1 0x10000000 capdl-loader-image-arm-tk1 bootelf 0x10000000 To which I get an error: No elf image at address 0x10000000 I tried with an older version of U-Boot (that worked following this same procedure about a year ago). It is U-Boot SPL 2014.10-rc2-g3127911 (Jun 07 2016 - 21:00:01) I also tried updating U-Boot to U-Boot SPL 2020.01-00442-gc00bd81ae0 (Jan 10 2020 - 11:10:18 -0500). Same error. Any thoughts or suggestions on how I get this to boot?

4 14