February 2020 - Devel - lists.sel4.systems

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

Question about MCS branch
by Isaac Beckett 06 Feb '20

06 Feb '20

I have a bit of a noobish question, why are timing/scheduling abilities being added to the kernel? I understand that userland still controls scheduling, regardless of which branch is being used, but I'm confused as to wby scheduling features needed to be added to the kernel itself.

2 1

Configuring CAmkES projects
by Grant Jurgensen 02 Feb '20

02 Feb '20

Hi everyone, I have a couple questions regarding the current CMake build structure for CAmkES projects. It seems that the current structure intends you to put your project in the camkes/apps folder, and then build your project with `../init-build -DCAMKES_APP=<project_name>`, or the equivalent using the griddle script. What I don't understand is how you are supposed to configure your project. It seems easy_settings.cmake is always loaded. Is it advisable to edit this file? In the past, I could also tweak configuration variables manually by invoking the ccmake gui on the top-level directory. Now that there is no CMakeLists.txt in the top-level directory, this does not work. If I try it in my project's directory, it tells me the cache is empty. Is it still possible to edit CMake cache variables with ccmake? Thanks! Grant Jurgensen

2 2

Recycle resources used by a thread after it terminates
by Alexandre Mutel 02 Feb '20

02 Feb '20

Hi, I have a design question regarding how to recycle capabilities/memory frames that were used by a thread once it terminates. Let's assume that there is a MemoryManager server responsible to serve virtual memory to user processes (e.g similar to implementing VirtualAlloc). The MemoryManager has to maintain the list of untyped object, retype them, maintain likely a list of resources allocated for a user thread, likely copy/mint the page frames to forward them to the user process...etc. But when a thread terminates, as I can't see any related events in seL4, I would assume that the user process would have to explicitly notify the MemoryManager on exit. Then the MemoryManager would know which user thread has exited and would update/recover the used capabilities and destroy them, in order to recover untyped objects. Would it be a proper design that plays well with seL4? Do you think that it could be done more efficiently with seL4? Thank you!

2 2