- Devel - lists.sel4.systems

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) 21 Feb '20

21 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 12 Feb '20

12 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 11 Feb '20

11 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

GPIO on Sabre imx6
by Parvaneh Ahgajani 10 Feb '20

10 Feb '20

Hello all, I am working with sabre lite board and using camkes framework. In my implementation I have a driver component that has 7 dataport buf and I connected these buffers to hardware component. In source of component driver I am initialize gpio_sys, mux_sys and pins using these functions: - imx6_mux_init() - imx6_gpio_sys_init() - gpio_new() Here I have copied some part of my code: ****************************************** gpio_sys_t gpio_sys; gpio_t pins[32*7]; mux_sys_t mux_sys; void gpio__init() { imx6_mux_init(NULL, &mux_sys); imx6_gpio_sys_init((void*)gpio0, (void*)gpio1, (void*)gpio2, (void*)gpio3, (void*)gpio4, (void*)gpio5, (void*)gpio6, &mux_sys, &gpio_sys); } void gpio_init_pin(int pin, int direction) { if(pin>0 && pin< sizeof(pins)/sizeof(pins[0])) { gpio_new(&gpio_sys, pin, (enum gpio_dir)direction, &pins[pin]); } } void gpio_set_pin(int pin, int value) { if(pin >= 0 && pin < (sizeof(pins)/sizeof(pins[0]))) { if(value) { gpio_set(&pins[pin]); } else { gpio_clr(&pins[pin]); } } } int gpio_read_pin(int pin) { if(pin>0 && pin< sizeof(pins)/sizeof(pins[0])) { return gpio_get(&pins[pin]); } return -1; } ****************************************** By calling "gpio_init_pin(ALARM_PIN= 28, 0);" I am getting this error: Assertion failed: bank->data == v (PATH/projects/util_libs/libplatsupport/src/plat/imx6/gpio.c: imx6_gpio_write: 144) How can I fix this error? How should I specify the GPIO pins? Thank you for your time and consideration, Parvaneh.

2 3

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

06 Feb '20

hi everybody i have quick questions regarding how can you take an input form terminal in seL4,i am trying to run a simple code of my own on sel4 and to display a message we use printf(), why scanf() is not working for me the way printf work.is there another way to do that

2 1